PG0006

polynomial_zero_extended_shift_reverse

Conversely every zero-extended value of an actual shift is the original zero-extended value; this is not formal polynomial equality.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ L. ∀ d. ∀ e. ∀ i. ∀ a. PolynomialShift(b,c,L,d,e) → BetaZeroExtend(d,e,S L,i,a) → BetaZeroExtend(b,c,L,i,a)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaZeroExtend(b,c,L,i,a) · 3PolynomialShift(b,c,L,d,e) · 1

Actual proof prerequisites

polynomial_zero_extended_entry_exists · checked external prerequisitepolynomial_zero_extended_entry_functional · checked external prerequisitepolynomial_zero_extended_shift_forward
Original expanded first-order statement 
forall b c L d e i a. (((forall mdr_i_pfp_shift_pad_reverse_relationprefix mdr_a_pfp_shift_pad_reverse_relationprefix. (exists mdr_gap_pfp_shift_pad_reverse_relationprefixb. mdr_gap_pfp_shift_pad_reverse_relationprefixb + S (mdr_i_pfp_shift_pad_reverse_relationprefix) = (L)) -> (((exists ff_h_mdr_pfp_shift_pad_reverse_relationprefixo. ff_h_mdr_pfp_shift_pad_reverse_relationprefixo + S (mdr_a_pfp_shift_pad_reverse_relationprefix) = S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * c)) /\ exists ff_q_mdr_pfp_shift_pad_reverse_relationprefixo. b = ff_q_mdr_pfp_shift_pad_reverse_relationprefixo * S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * c) + (mdr_a_pfp_shift_pad_reverse_relationprefix))) -> (((exists ff_h_mdr_pfp_shift_pad_reverse_relationprefixn. ff_h_mdr_pfp_shift_pad_reverse_relationprefixn + S (mdr_a_pfp_shift_pad_reverse_relationprefix) = S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * e)) /\ exists ff_q_mdr_pfp_shift_pad_reverse_relationprefixn. d = ff_q_mdr_pfp_shift_pad_reverse_relationprefixn * S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * e) + (mdr_a_pfp_shift_pad_reverse_relationprefix)))) /\ ((((exists ff_h_pfp_shift_pad_reverse_relationlast. ff_h_pfp_shift_pad_reverse_relationlast + S (0) = S ((S (L)) * e)) /\ exists ff_q_pfp_shift_pad_reverse_relationlast. d = ff_q_pfp_shift_pad_reverse_relationlast * S ((S (L)) * e) + (0)))))) -> ((((exists pfa_gap_shift_pad_reverse_sourceinside. pfa_gap_shift_pad_reverse_sourceinside + S (i) = (S L)) /\ ((((exists ff_h_pfp_shift_pad_reverse_sourceentry. ff_h_pfp_shift_pad_reverse_sourceentry + S (a) = S ((S (i)) * e)) /\ exists ff_q_pfp_shift_pad_reverse_sourceentry. d = ff_q_pfp_shift_pad_reverse_sourceentry * S ((S (i)) * e) + (a)))))) \/ (((exists pfc_gap_shift_pad_reverse_sourceoutside. pfc_gap_shift_pad_reverse_sourceoutside+(S L)=(i)) /\ (((a)=0))))) -> ((((exists pfa_gap_shift_pad_reverse_resultinside. pfa_gap_shift_pad_reverse_resultinside + S (i) = (L)) /\ ((((exists ff_h_pfp_shift_pad_reverse_resultentry. ff_h_pfp_shift_pad_reverse_resultentry + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_shift_pad_reverse_resultentry. b = ff_q_pfp_shift_pad_reverse_resultentry * S ((S (i)) * c) + (a)))))) \/ (((exists pfc_gap_shift_pad_reverse_resultoutside. pfc_gap_shift_pad_reverse_resultoutside+(L)=(i)) /\ (((a)=0)))))

Complete tactic proof in conservative notation

All 39 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

39 script commands · 7 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
polynomial zero extended shift forward
01Fix variables and assumptionsL1–9

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro L
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro i
  7. L7
    intro a
  8. L8
    intro hs
  9. L9
    intro ha
02Establish hxL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry exists.

  1. L10
    have hx : ∃ x. BetaZeroExtend(b,c,L,i,x)Definitions: BetaZeroExtend(b,c,L,i,x)Original native command in the exact edition
  2. L11
    specialize polynomial_zero_extended_entry_exists (b)
  3. L12
    specialize polynomial_zero_extended_entry_exists (c)
  4. L13
    specialize polynomial_zero_extended_entry_exists (L)
  5. L14
    specialize polynomial_zero_extended_entry_exists (i)
  6. L15
    apply polynomial_zero_extended_entry_exists
03Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    cases hx
04Establish heqL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry functional.

  1. L17
    have heq : a=x
  2. L18
    specialize polynomial_zero_extended_entry_functional (d)
  3. L19
    specialize polynomial_zero_extended_entry_functional (e)
  4. L20
    specialize polynomial_zero_extended_entry_functional (S L)
  5. L21
    specialize polynomial_zero_extended_entry_functional (i)
  6. L22
    specialize polynomial_zero_extended_entry_functional (a)
  7. L23
    specialize polynomial_zero_extended_entry_functional (x)
  8. L24
    apply polynomial_zero_extended_entry_functional
  9. L25
    exact ha
  10. L26
    specialize polynomial_zero_extended_shift_forward (b)
05Use earlier factsL27–35

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L27
    specialize polynomial_zero_extended_shift_forward (c)
  2. L28
    specialize polynomial_zero_extended_shift_forward (L)
  3. L29
    specialize polynomial_zero_extended_shift_forward (d)
  4. L30
    specialize polynomial_zero_extended_shift_forward (e)
  5. L31
    specialize polynomial_zero_extended_shift_forward (i)
  6. L32
    specialize polynomial_zero_extended_shift_forward (x)
  7. L33
    apply polynomial_zero_extended_shift_forward
  8. L34
    exact hs
  9. L35
    exact hx_witness
06Calculate and transport equalitiesL36–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L36
    rewrite heq
  2. L37
    rewrite heq
  3. L38
    rewrite heq
07Use earlier factsL39–39

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L39
    exact hx_witness

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro d
  5. 0005intro e
  6. 0006intro i
  7. 0007intro a
  8. 0008intro hs
  9. 0009intro ha
  10. 0010have hx : ∃ x. BetaZeroExtend(b,c,L,i,x)
  11. 0011specialize polynomial_zero_extended_entry_exists (b)
  12. 0012specialize polynomial_zero_extended_entry_exists (c)
  13. 0013specialize polynomial_zero_extended_entry_exists (L)
  14. 0014specialize polynomial_zero_extended_entry_exists (i)
  15. 0015apply polynomial_zero_extended_entry_exists
  16. 0016cases hx
  17. 0017have heq : a=x
  18. 0018specialize polynomial_zero_extended_entry_functional (d)
  19. 0019specialize polynomial_zero_extended_entry_functional (e)
  20. 0020specialize polynomial_zero_extended_entry_functional (S L)
  21. 0021specialize polynomial_zero_extended_entry_functional (i)
  22. 0022specialize polynomial_zero_extended_entry_functional (a)
  23. 0023specialize polynomial_zero_extended_entry_functional (x)
  24. 0024apply polynomial_zero_extended_entry_functional
  25. 0025exact ha
  26. 0026specialize polynomial_zero_extended_shift_forward (b)
  27. 0027specialize polynomial_zero_extended_shift_forward (c)
  28. 0028specialize polynomial_zero_extended_shift_forward (L)
  29. 0029specialize polynomial_zero_extended_shift_forward (d)
  30. 0030specialize polynomial_zero_extended_shift_forward (e)
  31. 0031specialize polynomial_zero_extended_shift_forward (i)
  32. 0032specialize polynomial_zero_extended_shift_forward (x)
  33. 0033apply polynomial_zero_extended_shift_forward
  34. 0034exact hs
  35. 0035exact hx_witness
  36. 0036rewrite heq
  37. 0037rewrite heq
  38. 0038rewrite heq
  39. 0039exact hx_witness