PG0005

polynomial_zero_extended_shift_forward

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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

Exact expanded first-order arithmetic 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)))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 47 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_succ Alpha theorem; checked-use authorized le_eq_or_lt Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized

Direct dependents

PG0006 polynomial_zero_extended_shift_reverse PG0007 polynomial_diagonal_term_shift_right_iff

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 \/ (exists pfa_gap_shift_pad_outside_order. pfa_gap_shift_pad_outside_order + S (L) = (i))
  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 exact 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 \/ (exists pfa_gap_shift_pad_outside_order. pfa_gap_shift_pad_outside_order + S (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