PX005E

polynomial_left_pad_natural_sum_invariant

Two actual natural sum traces have equal totals when one term prefix is the genuine leading-zero padding of the other.

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ B. ∀ C. ∀ t. ∀ L. ∀ n. ∀ m. PolynomialLeftPad(b,c,L,t,B,C) → Sum(b,c,L,n) → Sum(B,C,t + L,m) → m = n

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

Definition DAG

PolynomialLeftPad(b,c,L,t,d,e) · 2BetaAt(b,c,i,x) · 2Sum(b,c,l,z) · 4

Actual proof prerequisites

beta_sum_zero · checked external prerequisitebeta_repeat_sum_exact · checked external prerequisitele_succ · checked external prerequisitebeta_sum_succ_decompose · checked external prerequisitebeta_at_unique · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall b c B C t L n m. (((forall pfp_repeat_index_sum_pad_datazeros. (exists pfa_gap_sum_pad_datazerosindex. pfa_gap_sum_pad_datazerosindex + S (pfp_repeat_index_sum_pad_datazeros) = (t)) -> (((exists ff_h_pfp_sum_pad_datazerosentry. ff_h_pfp_sum_pad_datazerosentry + S (0) = S ((S (pfp_repeat_index_sum_pad_datazeros)) * C)) /\ exists ff_q_pfp_sum_pad_datazerosentry. B = ff_q_pfp_sum_pad_datazerosentry * S ((S (pfp_repeat_index_sum_pad_datazeros)) * C) + (0)))) /\ ((forall pfrep_index_sum_pad_data pfrep_value_sum_pad_data. (exists pfa_gap_sum_pad_databound. pfa_gap_sum_pad_databound + S (pfrep_index_sum_pad_data) = (L)) -> (((exists ff_h_pfp_sum_pad_datainput. ff_h_pfp_sum_pad_datainput + S (pfrep_value_sum_pad_data) = S ((S (pfrep_index_sum_pad_data)) * c)) /\ exists ff_q_pfp_sum_pad_datainput. b = ff_q_pfp_sum_pad_datainput * S ((S (pfrep_index_sum_pad_data)) * c) + (pfrep_value_sum_pad_data))) -> (((exists ff_h_pfp_sum_pad_dataoutput. ff_h_pfp_sum_pad_dataoutput + S (pfrep_value_sum_pad_data) = S ((S ((t)+pfrep_index_sum_pad_data)) * C)) /\ exists ff_q_pfp_sum_pad_dataoutput. B = ff_q_pfp_sum_pad_dataoutput * S ((S ((t)+pfrep_index_sum_pad_data)) * C) + (pfrep_value_sum_pad_data))))))) -> (exists fs_u_pfc_sum_pad_original fs_v_pfc_sum_pad_original. ((((exists fs_h_pfc_sum_pad_original_body_start. fs_h_pfc_sum_pad_original_body_start + S (0) = S ((S (0)) * fs_v_pfc_sum_pad_original)) /\ exists fs_q_pfc_sum_pad_original_body_start. fs_u_pfc_sum_pad_original = fs_q_pfc_sum_pad_original_body_start * S ((S (0)) * fs_v_pfc_sum_pad_original) + (0))) /\ ((((exists fs_h_pfc_sum_pad_original_body_terminal. fs_h_pfc_sum_pad_original_body_terminal + S (n) = S ((S (L)) * fs_v_pfc_sum_pad_original)) /\ exists fs_q_pfc_sum_pad_original_body_terminal. fs_u_pfc_sum_pad_original = fs_q_pfc_sum_pad_original_body_terminal * S ((S (L)) * fs_v_pfc_sum_pad_original) + (n))) /\ forall fs_i_pfc_sum_pad_original_body_steps. (exists fs_lt_pfc_sum_pad_original_body_steps_bound. fs_lt_pfc_sum_pad_original_body_steps_bound + S fs_i_pfc_sum_pad_original_body_steps = L) -> exists fs_a_pfc_sum_pad_original_body_steps fs_r_pfc_sum_pad_original_body_steps fs_s_pfc_sum_pad_original_body_steps. ((((exists fs_h_pfc_sum_pad_original_body_steps_summand. fs_h_pfc_sum_pad_original_body_steps_summand + S (fs_a_pfc_sum_pad_original_body_steps) = S ((S (fs_i_pfc_sum_pad_original_body_steps)) * c)) /\ exists fs_q_pfc_sum_pad_original_body_steps_summand. b = fs_q_pfc_sum_pad_original_body_steps_summand * S ((S (fs_i_pfc_sum_pad_original_body_steps)) * c) + (fs_a_pfc_sum_pad_original_body_steps))) /\ ((((exists fs_h_pfc_sum_pad_original_body_steps_partial. fs_h_pfc_sum_pad_original_body_steps_partial + S (fs_r_pfc_sum_pad_original_body_steps) = S ((S (fs_i_pfc_sum_pad_original_body_steps)) * fs_v_pfc_sum_pad_original)) /\ exists fs_q_pfc_sum_pad_original_body_steps_partial. fs_u_pfc_sum_pad_original = fs_q_pfc_sum_pad_original_body_steps_partial * S ((S (fs_i_pfc_sum_pad_original_body_steps)) * fs_v_pfc_sum_pad_original) + (fs_r_pfc_sum_pad_original_body_steps))) /\ ((((exists fs_h_pfc_sum_pad_original_body_steps_successor. fs_h_pfc_sum_pad_original_body_steps_successor + S (fs_s_pfc_sum_pad_original_body_steps) = S ((S (S fs_i_pfc_sum_pad_original_body_steps)) * fs_v_pfc_sum_pad_original)) /\ exists fs_q_pfc_sum_pad_original_body_steps_successor. fs_u_pfc_sum_pad_original = fs_q_pfc_sum_pad_original_body_steps_successor * S ((S (S fs_i_pfc_sum_pad_original_body_steps)) * fs_v_pfc_sum_pad_original) + (fs_s_pfc_sum_pad_original_body_steps))) /\ fs_s_pfc_sum_pad_original_body_steps = fs_r_pfc_sum_pad_original_body_steps + fs_a_pfc_sum_pad_original_body_steps)))))) -> (exists fs_u_pfc_sum_pad_actual fs_v_pfc_sum_pad_actual. ((((exists fs_h_pfc_sum_pad_actual_body_start. fs_h_pfc_sum_pad_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_sum_pad_actual)) /\ exists fs_q_pfc_sum_pad_actual_body_start. fs_u_pfc_sum_pad_actual = fs_q_pfc_sum_pad_actual_body_start * S ((S (0)) * fs_v_pfc_sum_pad_actual) + (0))) /\ ((((exists fs_h_pfc_sum_pad_actual_body_terminal. fs_h_pfc_sum_pad_actual_body_terminal + S (m) = S ((S (t+L)) * fs_v_pfc_sum_pad_actual)) /\ exists fs_q_pfc_sum_pad_actual_body_terminal. fs_u_pfc_sum_pad_actual = fs_q_pfc_sum_pad_actual_body_terminal * S ((S (t+L)) * fs_v_pfc_sum_pad_actual) + (m))) /\ forall fs_i_pfc_sum_pad_actual_body_steps. (exists fs_lt_pfc_sum_pad_actual_body_steps_bound. fs_lt_pfc_sum_pad_actual_body_steps_bound + S fs_i_pfc_sum_pad_actual_body_steps = t+L) -> exists fs_a_pfc_sum_pad_actual_body_steps fs_r_pfc_sum_pad_actual_body_steps fs_s_pfc_sum_pad_actual_body_steps. ((((exists fs_h_pfc_sum_pad_actual_body_steps_summand. fs_h_pfc_sum_pad_actual_body_steps_summand + S (fs_a_pfc_sum_pad_actual_body_steps) = S ((S (fs_i_pfc_sum_pad_actual_body_steps)) * C)) /\ exists fs_q_pfc_sum_pad_actual_body_steps_summand. B = fs_q_pfc_sum_pad_actual_body_steps_summand * S ((S (fs_i_pfc_sum_pad_actual_body_steps)) * C) + (fs_a_pfc_sum_pad_actual_body_steps))) /\ ((((exists fs_h_pfc_sum_pad_actual_body_steps_partial. fs_h_pfc_sum_pad_actual_body_steps_partial + S (fs_r_pfc_sum_pad_actual_body_steps) = S ((S (fs_i_pfc_sum_pad_actual_body_steps)) * fs_v_pfc_sum_pad_actual)) /\ exists fs_q_pfc_sum_pad_actual_body_steps_partial. fs_u_pfc_sum_pad_actual = fs_q_pfc_sum_pad_actual_body_steps_partial * S ((S (fs_i_pfc_sum_pad_actual_body_steps)) * fs_v_pfc_sum_pad_actual) + (fs_r_pfc_sum_pad_actual_body_steps))) /\ ((((exists fs_h_pfc_sum_pad_actual_body_steps_successor. fs_h_pfc_sum_pad_actual_body_steps_successor + S (fs_s_pfc_sum_pad_actual_body_steps) = S ((S (S fs_i_pfc_sum_pad_actual_body_steps)) * fs_v_pfc_sum_pad_actual)) /\ exists fs_q_pfc_sum_pad_actual_body_steps_successor. fs_u_pfc_sum_pad_actual = fs_q_pfc_sum_pad_actual_body_steps_successor * S ((S (S fs_i_pfc_sum_pad_actual_body_steps)) * fs_v_pfc_sum_pad_actual) + (fs_s_pfc_sum_pad_actual_body_steps))) /\ fs_s_pfc_sum_pad_actual_body_steps = fs_r_pfc_sum_pad_actual_body_steps + fs_a_pfc_sum_pad_actual_body_steps)))))) -> (m=n)

Complete tactic proof in conservative notation

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

113 script commands · 29 reading checkpoints · 8 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–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro B
  4. L4
    intro C
  5. L5
    intro t
02Induction on LL6–11

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction L
  2. L7
    intro n
  3. L8
    intro m
  4. L9
    intro hpad
  5. L10
    intro hs
  6. L11
    intro ht
03Separate the logical casesL12–12

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

  1. L12
    cases hpad
04Establish hnL13–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum zero.

  1. L13
    have hn : n=0
  2. L14
    specialize beta_sum_zero (b)
  3. L15
    specialize beta_sum_zero (c)
  4. L16
    specialize beta_sum_zero (n)
  5. L17
    apply beta_sum_zero
  6. L18
    exact hs
05Establish hlengthL19–28

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

  1. L19
    have hlength : t+0=t
  2. L20
    simp
  3. L21
    rewrite hlength at ht
  4. L22
    rewrite hlength at ht
  5. L23
    rewrite hlength at ht
  6. L24
    trans t*0
  7. L25
    specialize beta_repeat_sum_exact (B)
  8. L26
    specialize beta_repeat_sum_exact (C)
  9. L27
    specialize beta_repeat_sum_exact (0)
  10. L28
    specialize beta_repeat_sum_exact (t)
06Use earlier factsL29–32

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

  1. L29
    specialize beta_repeat_sum_exact (m)
  2. L30
    apply beta_repeat_sum_exact
  3. L31
    exact hpad_left
  4. L32
    exact ht
07Calculate and transport equalitiesL33–35

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

  1. L33
    trans 0
  2. L34
    simp
  3. L35
    symm
08Use earlier factsL36–36

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

  1. L36
    exact hn
09Fix variables and assumptionsL37–41

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

  1. L37
    intro n
  2. L38
    intro m
  3. L39
    intro hpad
  4. L40
    intro hs
  5. L41
    intro ht
10Separate the logical casesL42–42

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

  1. L42
    cases hpad
11Establish hpL43–43

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

  1. L43
    have hp : PolynomialLeftPad(b,c,L,t,B,C)Definitions: PolynomialLeftPad(b,c,L,t,B,C)Original native command in the exact edition
12Separate the logical casesL44–44

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

  1. L44
    split
13Use earlier factsL45–45

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

  1. L45
    exact hpad_left
14Fix variables and assumptionsL46–49

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

  1. L46
    intro i
  2. L47
    intro a
  3. L48
    intro hi
  4. L49
    intro ha
15Use earlier factsL50–57

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

  1. L50
    specialize hpad_right (i)
  2. L51
    specialize hpad_right (a)
  3. L52
    apply hpad_right
  4. L53
    specialize le_succ (S i)
  5. L54
    specialize le_succ (L)
  6. L55
    apply le_succ
  7. L56
    exact hi
  8. L57
    exact ha
16Establish hfirstL58–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L58
    have hfirst : ∃ a. ∃ u. BetaAt(b,c,L,a) ∧ (Sum(b,c,L,u) ∧ n = u + a)Definitions: BetaAt(b,c,L,a)Sum(b,c,L,u)Original native command in the exact edition
  2. L59
    specialize beta_sum_succ_decompose (b)
  3. L60
    specialize beta_sum_succ_decompose (c)
  4. L61
    specialize beta_sum_succ_decompose (L)
  5. L62
    specialize beta_sum_succ_decompose (n)
  6. L63
    apply beta_sum_succ_decompose
  7. L64
    exact hs
17Separate the logical casesL65–68

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

  1. L65
    cases hfirst
  2. L66
    cases hfirst_witness
  3. L67
    cases hfirst_witness_witness
  4. L68
    cases hfirst_witness_witness_right
18Establish hlengthL69–73

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

  1. L69
    have hlength : t+S L=S (t+L)
  2. L70
    simp
  3. L71
    rewrite hlength at ht
  4. L72
    rewrite hlength at ht
  5. L73
    rewrite hlength at ht
19Establish hsecondL74–80

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L74
    have hsecond : ∃ a. ∃ u. BetaAt(B,C,t + L,a) ∧ (Sum(B,C,t + L,u) ∧ m = u + a)Definitions: BetaAt(B,C,t + L,a)Sum(B,C,t + L,u)Original native command in the exact edition
  2. L75
    specialize beta_sum_succ_decompose (B)
  3. L76
    specialize beta_sum_succ_decompose (C)
  4. L77
    specialize beta_sum_succ_decompose (t+L)
  5. L78
    specialize beta_sum_succ_decompose (m)
  6. L79
    apply beta_sum_succ_decompose
  7. L80
    exact ht
20Separate the logical casesL81–84

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

  1. L81
    cases hsecond
  2. L82
    cases hsecond_witness
  3. L83
    cases hsecond_witness_witness
  4. L84
    cases hsecond_witness_witness_right
21Establish hprefixL85–91

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L85
    have hprefix : x3=x1
  2. L86
    specialize IH (x1)
  3. L87
    specialize IH (x3)
  4. L88
    apply IH
  5. L89
    exact hp
  6. L90
    exact hfirst_witness_witness_right_left
  7. L91
    exact hsecond_witness_witness_right_left
22Establish hentryL92–101

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L92
    have hentry : x2=x
  2. L93
    specialize beta_at_unique (B)
  3. L94
    specialize beta_at_unique (C)
  4. L95
    specialize beta_at_unique (t+L)
  5. L96
    specialize beta_at_unique (x2)
  6. L97
    specialize beta_at_unique (x)
  7. L98
    apply beta_at_unique
  8. L99
    exact hsecond_witness_witness_left
  9. L100
    specialize hpad_right (L)
  10. L101
    specialize hpad_right (x)
23Use earlier factsL102–105

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

  1. L102
    apply hpad_right
  2. L103
    specialize le_refl (S L)
  3. L104
    apply le_refl
  4. L105
    exact hfirst_witness_witness_left
24Calculate and transport equalitiesL106–106

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

  1. L106
    trans x3+x2
25Use earlier factsL107–107

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

  1. L107
    exact hsecond_witness_witness_right_right
26Calculate and transport equalitiesL108–109

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

  1. L108
    trans x1+x
  2. L109
    congr
27Use earlier factsL110–111

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

  1. L110
    exact hprefix
  2. L111
    exact hentry
28Calculate and transport equalitiesL112–112

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

  1. L112
    symm
29Use earlier factsL113–113

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

  1. L113
    exact hfirst_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 113 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro B
  4. 0004intro C
  5. 0005intro t
  6. 0006induction L
  7. 0007intro n
  8. 0008intro m
  9. 0009intro hpad
  10. 0010intro hs
  11. 0011intro ht
  12. 0012cases hpad
  13. 0013have hn : n=0
  14. 0014specialize beta_sum_zero (b)
  15. 0015specialize beta_sum_zero (c)
  16. 0016specialize beta_sum_zero (n)
  17. 0017apply beta_sum_zero
  18. 0018exact hs
  19. 0019have hlength : t+0=t
  20. 0020simp
  21. 0021rewrite hlength at ht
  22. 0022rewrite hlength at ht
  23. 0023rewrite hlength at ht
  24. 0024trans t*0
  25. 0025specialize beta_repeat_sum_exact (B)
  26. 0026specialize beta_repeat_sum_exact (C)
  27. 0027specialize beta_repeat_sum_exact (0)
  28. 0028specialize beta_repeat_sum_exact (t)
  29. 0029specialize beta_repeat_sum_exact (m)
  30. 0030apply beta_repeat_sum_exact
  31. 0031exact hpad_left
  32. 0032exact ht
  33. 0033trans 0
  34. 0034simp
  35. 0035symm
  36. 0036exact hn
  37. 0037intro n
  38. 0038intro m
  39. 0039intro hpad
  40. 0040intro hs
  41. 0041intro ht
  42. 0042cases hpad
  43. 0043have hp : PolynomialLeftPad(b,c,L,t,B,C)
  44. 0044split
  45. 0045exact hpad_left
  46. 0046intro i
  47. 0047intro a
  48. 0048intro hi
  49. 0049intro ha
  50. 0050specialize hpad_right (i)
  51. 0051specialize hpad_right (a)
  52. 0052apply hpad_right
  53. 0053specialize le_succ (S i)
  54. 0054specialize le_succ (L)
  55. 0055apply le_succ
  56. 0056exact hi
  57. 0057exact ha
  58. 0058have hfirst : ∃ a. ∃ u. BetaAt(b,c,L,a) ∧ (Sum(b,c,L,u) ∧ n = u + a)
  59. 0059specialize beta_sum_succ_decompose (b)
  60. 0060specialize beta_sum_succ_decompose (c)
  61. 0061specialize beta_sum_succ_decompose (L)
  62. 0062specialize beta_sum_succ_decompose (n)
  63. 0063apply beta_sum_succ_decompose
  64. 0064exact hs
  65. 0065cases hfirst
  66. 0066cases hfirst_witness
  67. 0067cases hfirst_witness_witness
  68. 0068cases hfirst_witness_witness_right
  69. 0069have hlength : t+S L=S (t+L)
  70. 0070simp
  71. 0071rewrite hlength at ht
  72. 0072rewrite hlength at ht
  73. 0073rewrite hlength at ht
  74. 0074have hsecond : ∃ a. ∃ u. BetaAt(B,C,t + L,a) ∧ (Sum(B,C,t + L,u) ∧ m = u + a)
  75. 0075specialize beta_sum_succ_decompose (B)
  76. 0076specialize beta_sum_succ_decompose (C)
  77. 0077specialize beta_sum_succ_decompose (t+L)
  78. 0078specialize beta_sum_succ_decompose (m)
  79. 0079apply beta_sum_succ_decompose
  80. 0080exact ht
  81. 0081cases hsecond
  82. 0082cases hsecond_witness
  83. 0083cases hsecond_witness_witness
  84. 0084cases hsecond_witness_witness_right
  85. 0085have hprefix : x3=x1
  86. 0086specialize IH (x1)
  87. 0087specialize IH (x3)
  88. 0088apply IH
  89. 0089exact hp
  90. 0090exact hfirst_witness_witness_right_left
  91. 0091exact hsecond_witness_witness_right_left
  92. 0092have hentry : x2=x
  93. 0093specialize beta_at_unique (B)
  94. 0094specialize beta_at_unique (C)
  95. 0095specialize beta_at_unique (t+L)
  96. 0096specialize beta_at_unique (x2)
  97. 0097specialize beta_at_unique (x)
  98. 0098apply beta_at_unique
  99. 0099exact hsecond_witness_witness_left
  100. 0100specialize hpad_right (L)
  101. 0101specialize hpad_right (x)
  102. 0102apply hpad_right
  103. 0103specialize le_refl (S L)
  104. 0104apply le_refl
  105. 0105exact hfirst_witness_witness_left
  106. 0106trans x3+x2
  107. 0107exact hsecond_witness_witness_right_right
  108. 0108trans x1+x
  109. 0109congr
  110. 0110exact hprefix
  111. 0111exact hentry
  112. 0112symm
  113. 0113exact hfirst_witness_witness_right_right