PX005F

polynomial_zero_tail_natural_sum_invariant

Appending a genuinely all-zero tail to an independently recoded natural summand prefix preserves its actual sum.

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. ∀ L. ∀ t. ∀ n. ∀ m. BetaPrefixEqual(b,c,B,C,L) → (∀ x. Lt(x,t) → BetaAt(B,C,L + x,0)) → Sum(b,c,L,n) → Sum(B,C,L + t,m) → m = n

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 2Sum(b,c,l,z) · 3

Actual proof prerequisites

beta_sum_functional · checked external prerequisitebeta_sum_transport_prefix · checked external prerequisitebeta_sum_succ_decompose · checked external prerequisitele_succ · checked external prerequisitebeta_at_unique · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall b c B C L t n m. (forall mdr_i_pfp_sum_tail_equal mdr_a_pfp_sum_tail_equal. (exists mdr_gap_pfp_sum_tail_equalb. mdr_gap_pfp_sum_tail_equalb + S (mdr_i_pfp_sum_tail_equal) = (L)) -> (((exists ff_h_mdr_pfp_sum_tail_equalo. ff_h_mdr_pfp_sum_tail_equalo + S (mdr_a_pfp_sum_tail_equal) = S ((S (mdr_i_pfp_sum_tail_equal)) * c)) /\ exists ff_q_mdr_pfp_sum_tail_equalo. b = ff_q_mdr_pfp_sum_tail_equalo * S ((S (mdr_i_pfp_sum_tail_equal)) * c) + (mdr_a_pfp_sum_tail_equal))) -> (((exists ff_h_mdr_pfp_sum_tail_equaln. ff_h_mdr_pfp_sum_tail_equaln + S (mdr_a_pfp_sum_tail_equal) = S ((S (mdr_i_pfp_sum_tail_equal)) * C)) /\ exists ff_q_mdr_pfp_sum_tail_equaln. B = ff_q_mdr_pfp_sum_tail_equaln * S ((S (mdr_i_pfp_sum_tail_equal)) * C) + (mdr_a_pfp_sum_tail_equal)))) -> (forall pfpad_tail_index_sum_tail_zero. (exists pfa_gap_sum_tail_zerobound. pfa_gap_sum_tail_zerobound + S (pfpad_tail_index_sum_tail_zero) = (t)) -> (((exists ff_h_pfp_sum_tail_zerozero. ff_h_pfp_sum_tail_zerozero + S (0) = S ((S ((L)+pfpad_tail_index_sum_tail_zero)) * C)) /\ exists ff_q_pfp_sum_tail_zerozero. B = ff_q_pfp_sum_tail_zerozero * S ((S ((L)+pfpad_tail_index_sum_tail_zero)) * C) + (0)))) -> (exists fs_u_pfc_sum_tail_original fs_v_pfc_sum_tail_original. ((((exists fs_h_pfc_sum_tail_original_body_start. fs_h_pfc_sum_tail_original_body_start + S (0) = S ((S (0)) * fs_v_pfc_sum_tail_original)) /\ exists fs_q_pfc_sum_tail_original_body_start. fs_u_pfc_sum_tail_original = fs_q_pfc_sum_tail_original_body_start * S ((S (0)) * fs_v_pfc_sum_tail_original) + (0))) /\ ((((exists fs_h_pfc_sum_tail_original_body_terminal. fs_h_pfc_sum_tail_original_body_terminal + S (n) = S ((S (L)) * fs_v_pfc_sum_tail_original)) /\ exists fs_q_pfc_sum_tail_original_body_terminal. fs_u_pfc_sum_tail_original = fs_q_pfc_sum_tail_original_body_terminal * S ((S (L)) * fs_v_pfc_sum_tail_original) + (n))) /\ forall fs_i_pfc_sum_tail_original_body_steps. (exists fs_lt_pfc_sum_tail_original_body_steps_bound. fs_lt_pfc_sum_tail_original_body_steps_bound + S fs_i_pfc_sum_tail_original_body_steps = L) -> exists fs_a_pfc_sum_tail_original_body_steps fs_r_pfc_sum_tail_original_body_steps fs_s_pfc_sum_tail_original_body_steps. ((((exists fs_h_pfc_sum_tail_original_body_steps_summand. fs_h_pfc_sum_tail_original_body_steps_summand + S (fs_a_pfc_sum_tail_original_body_steps) = S ((S (fs_i_pfc_sum_tail_original_body_steps)) * c)) /\ exists fs_q_pfc_sum_tail_original_body_steps_summand. b = fs_q_pfc_sum_tail_original_body_steps_summand * S ((S (fs_i_pfc_sum_tail_original_body_steps)) * c) + (fs_a_pfc_sum_tail_original_body_steps))) /\ ((((exists fs_h_pfc_sum_tail_original_body_steps_partial. fs_h_pfc_sum_tail_original_body_steps_partial + S (fs_r_pfc_sum_tail_original_body_steps) = S ((S (fs_i_pfc_sum_tail_original_body_steps)) * fs_v_pfc_sum_tail_original)) /\ exists fs_q_pfc_sum_tail_original_body_steps_partial. fs_u_pfc_sum_tail_original = fs_q_pfc_sum_tail_original_body_steps_partial * S ((S (fs_i_pfc_sum_tail_original_body_steps)) * fs_v_pfc_sum_tail_original) + (fs_r_pfc_sum_tail_original_body_steps))) /\ ((((exists fs_h_pfc_sum_tail_original_body_steps_successor. fs_h_pfc_sum_tail_original_body_steps_successor + S (fs_s_pfc_sum_tail_original_body_steps) = S ((S (S fs_i_pfc_sum_tail_original_body_steps)) * fs_v_pfc_sum_tail_original)) /\ exists fs_q_pfc_sum_tail_original_body_steps_successor. fs_u_pfc_sum_tail_original = fs_q_pfc_sum_tail_original_body_steps_successor * S ((S (S fs_i_pfc_sum_tail_original_body_steps)) * fs_v_pfc_sum_tail_original) + (fs_s_pfc_sum_tail_original_body_steps))) /\ fs_s_pfc_sum_tail_original_body_steps = fs_r_pfc_sum_tail_original_body_steps + fs_a_pfc_sum_tail_original_body_steps)))))) -> (exists fs_u_pfc_sum_tail_actual fs_v_pfc_sum_tail_actual. ((((exists fs_h_pfc_sum_tail_actual_body_start. fs_h_pfc_sum_tail_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_sum_tail_actual)) /\ exists fs_q_pfc_sum_tail_actual_body_start. fs_u_pfc_sum_tail_actual = fs_q_pfc_sum_tail_actual_body_start * S ((S (0)) * fs_v_pfc_sum_tail_actual) + (0))) /\ ((((exists fs_h_pfc_sum_tail_actual_body_terminal. fs_h_pfc_sum_tail_actual_body_terminal + S (m) = S ((S (L+t)) * fs_v_pfc_sum_tail_actual)) /\ exists fs_q_pfc_sum_tail_actual_body_terminal. fs_u_pfc_sum_tail_actual = fs_q_pfc_sum_tail_actual_body_terminal * S ((S (L+t)) * fs_v_pfc_sum_tail_actual) + (m))) /\ forall fs_i_pfc_sum_tail_actual_body_steps. (exists fs_lt_pfc_sum_tail_actual_body_steps_bound. fs_lt_pfc_sum_tail_actual_body_steps_bound + S fs_i_pfc_sum_tail_actual_body_steps = L+t) -> exists fs_a_pfc_sum_tail_actual_body_steps fs_r_pfc_sum_tail_actual_body_steps fs_s_pfc_sum_tail_actual_body_steps. ((((exists fs_h_pfc_sum_tail_actual_body_steps_summand. fs_h_pfc_sum_tail_actual_body_steps_summand + S (fs_a_pfc_sum_tail_actual_body_steps) = S ((S (fs_i_pfc_sum_tail_actual_body_steps)) * C)) /\ exists fs_q_pfc_sum_tail_actual_body_steps_summand. B = fs_q_pfc_sum_tail_actual_body_steps_summand * S ((S (fs_i_pfc_sum_tail_actual_body_steps)) * C) + (fs_a_pfc_sum_tail_actual_body_steps))) /\ ((((exists fs_h_pfc_sum_tail_actual_body_steps_partial. fs_h_pfc_sum_tail_actual_body_steps_partial + S (fs_r_pfc_sum_tail_actual_body_steps) = S ((S (fs_i_pfc_sum_tail_actual_body_steps)) * fs_v_pfc_sum_tail_actual)) /\ exists fs_q_pfc_sum_tail_actual_body_steps_partial. fs_u_pfc_sum_tail_actual = fs_q_pfc_sum_tail_actual_body_steps_partial * S ((S (fs_i_pfc_sum_tail_actual_body_steps)) * fs_v_pfc_sum_tail_actual) + (fs_r_pfc_sum_tail_actual_body_steps))) /\ ((((exists fs_h_pfc_sum_tail_actual_body_steps_successor. fs_h_pfc_sum_tail_actual_body_steps_successor + S (fs_s_pfc_sum_tail_actual_body_steps) = S ((S (S fs_i_pfc_sum_tail_actual_body_steps)) * fs_v_pfc_sum_tail_actual)) /\ exists fs_q_pfc_sum_tail_actual_body_steps_successor. fs_u_pfc_sum_tail_actual = fs_q_pfc_sum_tail_actual_body_steps_successor * S ((S (S fs_i_pfc_sum_tail_actual_body_steps)) * fs_v_pfc_sum_tail_actual) + (fs_s_pfc_sum_tail_actual_body_steps))) /\ fs_s_pfc_sum_tail_actual_body_steps = fs_r_pfc_sum_tail_actual_body_steps + fs_a_pfc_sum_tail_actual_body_steps)))))) -> (m=n)

Complete tactic proof in conservative notation

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

88 script commands · 17 reading checkpoints · 5 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 L
02Induction on tL6–12

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

  1. L6
    induction t
  2. L7
    intro n
  3. L8
    intro m
  4. L9
    intro he
  5. L10
    intro hz
  6. L11
    intro hs
  7. L12
    intro ht
03Establish hlengthL13–22

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

  1. L13
    have hlength : L+0=L
  2. L14
    simp
  3. L15
    rewrite hlength at ht
  4. L16
    rewrite hlength at ht
  5. L17
    rewrite hlength at ht
  6. L18
    specialize beta_sum_functional (B)
  7. L19
    specialize beta_sum_functional (C)
  8. L20
    specialize beta_sum_functional (L)
  9. L21
    specialize beta_sum_functional (m)
  10. L22
    specialize beta_sum_functional (n)
04Use earlier factsL23–32

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

  1. L23
    apply beta_sum_functional
  2. L24
    exact ht
  3. L25
    specialize beta_sum_transport_prefix (b)
  4. L26
    specialize beta_sum_transport_prefix (c)
  5. L27
    specialize beta_sum_transport_prefix (B)
  6. L28
    specialize beta_sum_transport_prefix (C)
  7. L29
    specialize beta_sum_transport_prefix (L)
  8. L30
    specialize beta_sum_transport_prefix (n)
  9. L31
    apply beta_sum_transport_prefix
  10. L32
    exact hs
05Use earlier factsL33–33

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

  1. L33
    exact he
06Fix variables and assumptionsL34–39

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

  1. L34
    intro n
  2. L35
    intro m
  3. L36
    intro he
  4. L37
    intro hz
  5. L38
    intro hs
  6. L39
    intro ht
07Establish hlengthL40–44

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

  1. L40
    have hlength : L+S t=S (L+t)
  2. L41
    simp
  3. L42
    rewrite hlength at ht
  4. L43
    rewrite hlength at ht
  5. L44
    rewrite hlength at ht
08Establish hdL45–51

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

  1. L45
    have hd : ∃ a. ∃ u. BetaAt(B,C,L + t,a) ∧ (Sum(B,C,L + t,u) ∧ m = u + a)Definitions: BetaAt(B,C,L + t,a)Sum(B,C,L + t,u)Original native command in the exact edition
  2. L46
    specialize beta_sum_succ_decompose (B)
  3. L47
    specialize beta_sum_succ_decompose (C)
  4. L48
    specialize beta_sum_succ_decompose (L+t)
  5. L49
    specialize beta_sum_succ_decompose (m)
  6. L50
    apply beta_sum_succ_decompose
  7. L51
    exact ht
09Separate the logical casesL52–55

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

  1. L52
    cases hd
  2. L53
    cases hd_witness
  3. L54
    cases hd_witness_witness
  4. L55
    cases hd_witness_witness_right
10Establish hprefixL56–65

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

  1. L56
    have hprefix : x1=n
  2. L57
    specialize IH (n)
  3. L58
    specialize IH (x1)
  4. L59
    apply IH
  5. L60
    exact he
  6. L61
    intro i
  7. L62
    intro hi
  8. L63
    specialize hz (i)
  9. L64
    apply hz
  10. L65
    specialize le_succ (S i)
11Use earlier factsL66–70

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

  1. L66
    specialize le_succ (t)
  2. L67
    apply le_succ
  3. L68
    exact hi
  4. L69
    exact hs
  5. L70
    exact hd_witness_witness_right_left
12Establish hzeroL71–80

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

  1. L71
    have hzero : x=0
  2. L72
    specialize beta_at_unique (B)
  3. L73
    specialize beta_at_unique (C)
  4. L74
    specialize beta_at_unique (L+t)
  5. L75
    specialize beta_at_unique (x)
  6. L76
    specialize beta_at_unique (0)
  7. L77
    apply beta_at_unique
  8. L78
    exact hd_witness_witness_left
  9. L79
    specialize hz (t)
  10. L80
    apply hz
13Use earlier factsL81–82

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

  1. L81
    specialize le_refl (S t)
  2. L82
    apply le_refl
14Calculate and transport equalitiesL83–83

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

  1. L83
    trans x1+x
15Use earlier factsL84–84

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

  1. L84
    exact hd_witness_witness_right_right
16Calculate and transport equalitiesL85–87

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

  1. L85
    trans x1
  2. L86
    rewrite hzero
  3. L87
    simp
17Use earlier factsL88–88

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

  1. L88
    exact hprefix

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro B
  4. 0004intro C
  5. 0005intro L
  6. 0006induction t
  7. 0007intro n
  8. 0008intro m
  9. 0009intro he
  10. 0010intro hz
  11. 0011intro hs
  12. 0012intro ht
  13. 0013have hlength : L+0=L
  14. 0014simp
  15. 0015rewrite hlength at ht
  16. 0016rewrite hlength at ht
  17. 0017rewrite hlength at ht
  18. 0018specialize beta_sum_functional (B)
  19. 0019specialize beta_sum_functional (C)
  20. 0020specialize beta_sum_functional (L)
  21. 0021specialize beta_sum_functional (m)
  22. 0022specialize beta_sum_functional (n)
  23. 0023apply beta_sum_functional
  24. 0024exact ht
  25. 0025specialize beta_sum_transport_prefix (b)
  26. 0026specialize beta_sum_transport_prefix (c)
  27. 0027specialize beta_sum_transport_prefix (B)
  28. 0028specialize beta_sum_transport_prefix (C)
  29. 0029specialize beta_sum_transport_prefix (L)
  30. 0030specialize beta_sum_transport_prefix (n)
  31. 0031apply beta_sum_transport_prefix
  32. 0032exact hs
  33. 0033exact he
  34. 0034intro n
  35. 0035intro m
  36. 0036intro he
  37. 0037intro hz
  38. 0038intro hs
  39. 0039intro ht
  40. 0040have hlength : L+S t=S (L+t)
  41. 0041simp
  42. 0042rewrite hlength at ht
  43. 0043rewrite hlength at ht
  44. 0044rewrite hlength at ht
  45. 0045have hd : ∃ a. ∃ u. BetaAt(B,C,L + t,a) ∧ (Sum(B,C,L + t,u) ∧ m = u + a)
  46. 0046specialize beta_sum_succ_decompose (B)
  47. 0047specialize beta_sum_succ_decompose (C)
  48. 0048specialize beta_sum_succ_decompose (L+t)
  49. 0049specialize beta_sum_succ_decompose (m)
  50. 0050apply beta_sum_succ_decompose
  51. 0051exact ht
  52. 0052cases hd
  53. 0053cases hd_witness
  54. 0054cases hd_witness_witness
  55. 0055cases hd_witness_witness_right
  56. 0056have hprefix : x1=n
  57. 0057specialize IH (n)
  58. 0058specialize IH (x1)
  59. 0059apply IH
  60. 0060exact he
  61. 0061intro i
  62. 0062intro hi
  63. 0063specialize hz (i)
  64. 0064apply hz
  65. 0065specialize le_succ (S i)
  66. 0066specialize le_succ (t)
  67. 0067apply le_succ
  68. 0068exact hi
  69. 0069exact hs
  70. 0070exact hd_witness_witness_right_left
  71. 0071have hzero : x=0
  72. 0072specialize beta_at_unique (B)
  73. 0073specialize beta_at_unique (C)
  74. 0074specialize beta_at_unique (L+t)
  75. 0075specialize beta_at_unique (x)
  76. 0076specialize beta_at_unique (0)
  77. 0077apply beta_at_unique
  78. 0078exact hd_witness_witness_left
  79. 0079specialize hz (t)
  80. 0080apply hz
  81. 0081specialize le_refl (S t)
  82. 0082apply le_refl
  83. 0083trans x1+x
  84. 0084exact hd_witness_witness_right_right
  85. 0085trans x1
  86. 0086rewrite hzero
  87. 0087simp
  88. 0088exact hprefix