PG0005

polynomial_zero_extended_shift_forward

Trailing-zero extension leaves each actual zero-extended array value unchanged, at every natural index.

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(b,c,L,i,a) → BetaZeroExtend(d,e,S L,i,a)

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

Definition DAG

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

Actual proof prerequisites

le_succ · checked external prerequisitele_eq_or_lt · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall b c L d e i a. (((forall mdr_i_pfp_shift_pad_relationprefix mdr_a_pfp_shift_pad_relationprefix. (exists mdr_gap_pfp_shift_pad_relationprefixb. mdr_gap_pfp_shift_pad_relationprefixb + S (mdr_i_pfp_shift_pad_relationprefix) = (L)) -> (((exists ff_h_mdr_pfp_shift_pad_relationprefixo. ff_h_mdr_pfp_shift_pad_relationprefixo + S (mdr_a_pfp_shift_pad_relationprefix) = S ((S (mdr_i_pfp_shift_pad_relationprefix)) * c)) /\ exists ff_q_mdr_pfp_shift_pad_relationprefixo. b = ff_q_mdr_pfp_shift_pad_relationprefixo * S ((S (mdr_i_pfp_shift_pad_relationprefix)) * c) + (mdr_a_pfp_shift_pad_relationprefix))) -> (((exists ff_h_mdr_pfp_shift_pad_relationprefixn. ff_h_mdr_pfp_shift_pad_relationprefixn + S (mdr_a_pfp_shift_pad_relationprefix) = S ((S (mdr_i_pfp_shift_pad_relationprefix)) * e)) /\ exists ff_q_mdr_pfp_shift_pad_relationprefixn. d = ff_q_mdr_pfp_shift_pad_relationprefixn * S ((S (mdr_i_pfp_shift_pad_relationprefix)) * e) + (mdr_a_pfp_shift_pad_relationprefix)))) /\ ((((exists ff_h_pfp_shift_pad_relationlast. ff_h_pfp_shift_pad_relationlast + S (0) = S ((S (L)) * e)) /\ exists ff_q_pfp_shift_pad_relationlast. d = ff_q_pfp_shift_pad_relationlast * S ((S (L)) * e) + (0)))))) -> ((((exists pfa_gap_shift_pad_sourceinside. pfa_gap_shift_pad_sourceinside + S (i) = (L)) /\ ((((exists ff_h_pfp_shift_pad_sourceentry. ff_h_pfp_shift_pad_sourceentry + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_shift_pad_sourceentry. b = ff_q_pfp_shift_pad_sourceentry * S ((S (i)) * c) + (a)))))) \/ (((exists pfc_gap_shift_pad_sourceoutside. pfc_gap_shift_pad_sourceoutside+(L)=(i)) /\ (((a)=0))))) -> ((((exists pfa_gap_shift_pad_targetinside. pfa_gap_shift_pad_targetinside + S (i) = (S L)) /\ ((((exists ff_h_pfp_shift_pad_targetentry. ff_h_pfp_shift_pad_targetentry + S (a) = S ((S (i)) * e)) /\ exists ff_q_pfp_shift_pad_targetentry. d = ff_q_pfp_shift_pad_targetentry * S ((S (i)) * e) + (a)))))) \/ (((exists pfc_gap_shift_pad_targetoutside. pfc_gap_shift_pad_targetoutside+(S L)=(i)) /\ (((a)=0)))))

Complete tactic proof in conservative notation

All 47 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

47 script commands · 14 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.

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
02Separate the logical casesL10–14

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

  1. L10
    cases hs
  2. L11
    cases ha
  3. L12
    cases ha_left
  4. L13
    left
  5. L14
    split
03Use earlier factsL15–23

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

  1. L15
    specialize le_succ (S i)
  2. L16
    specialize le_succ (L)
  3. L17
    apply le_succ
  4. L18
    exact ha_left_left
  5. L19
    specialize hs_left (i)
  6. L20
    specialize hs_left (a)
  7. L21
    apply hs_left
  8. L22
    exact ha_left_left
  9. L23
    exact ha_left_right
04Separate the logical casesL24–24

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

  1. L24
    cases ha_right
05Establish hoL25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L25
    have ho : L = i ∨ Lt(L,i)Definitions: Lt(L,i)Original native command in the exact edition
  2. L26
    specialize le_eq_or_lt (L)
  3. L27
    specialize le_eq_or_lt (i)
  4. L28
    apply le_eq_or_lt
  5. L29
    exact ha_right_left
06Separate the logical casesL30–30

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

  1. L30
    cases ho
07Establish hiiL31–33

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hii : i=L
  2. L32
    symm
  3. L33
    exact ho_left
08Separate the logical casesL34–35

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

  1. L34
    left
  2. L35
    split
09Calculate and transport equalitiesL36–36

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

  1. L36
    rewrite hii
10Use earlier factsL37–38

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

  1. L37
    specialize le_refl (S L)
  2. L38
    apply le_refl
11Calculate and transport equalitiesL39–42

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

  1. L39
    rewrite hii
  2. L40
    rewrite hii
  3. L41
    rewrite ha_right_right
  4. L42
    rewrite ha_right_right
12Use earlier factsL43–43

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

  1. L43
    exact hs_right
13Separate the logical casesL44–45

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

  1. L44
    right
  2. L45
    split
14Use earlier factsL46–47

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

  1. L46
    exact ho_right
  2. L47
    exact ha_right_right

Library-wide reading audit

Original defined command ledger · 47 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. 0010cases hs
  11. 0011cases ha
  12. 0012cases ha_left
  13. 0013left
  14. 0014split
  15. 0015specialize le_succ (S i)
  16. 0016specialize le_succ (L)
  17. 0017apply le_succ
  18. 0018exact ha_left_left
  19. 0019specialize hs_left (i)
  20. 0020specialize hs_left (a)
  21. 0021apply hs_left
  22. 0022exact ha_left_left
  23. 0023exact ha_left_right
  24. 0024cases ha_right
  25. 0025have ho : L = i ∨ Lt(L,i)
  26. 0026specialize le_eq_or_lt (L)
  27. 0027specialize le_eq_or_lt (i)
  28. 0028apply le_eq_or_lt
  29. 0029exact ha_right_left
  30. 0030cases ho
  31. 0031have hii : i=L
  32. 0032symm
  33. 0033exact ho_left
  34. 0034left
  35. 0035split
  36. 0036rewrite hii
  37. 0037specialize le_refl (S L)
  38. 0038apply le_refl
  39. 0039rewrite hii
  40. 0040rewrite hii
  41. 0041rewrite ha_right_right
  42. 0042rewrite ha_right_right
  43. 0043exact hs_right
  44. 0044right
  45. 0045split
  46. 0046exact ho_right
  47. 0047exact ha_right_right