SS0012

divisor_natural_sum_successor_intro

The successor natural sum is genuinely constructed and identified with the previous sum plus the actual last beta entry.

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

These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ r. ∀ a. Sum(b,c,l,r) → BetaAt(b,c,l,a) → Sum(b,c,S l,r + a)

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

Definition DAG

BetaAt(b,c,i,x) · 2Sum(b,c,l,z) · 4

Actual proof prerequisites

beta_sum_exists · checked external prerequisitebeta_sum_succ_decompose · checked external prerequisitebeta_at_unique · checked external prerequisitebeta_sum_functional · checked external prerequisite
Original expanded first-order statement 
forall b c l r a. (exists fs_u_dst_natural_step_prefix fs_v_dst_natural_step_prefix. ((((exists fs_h_dst_natural_step_prefix_body_start. fs_h_dst_natural_step_prefix_body_start + S (0) = S ((S (0)) * fs_v_dst_natural_step_prefix)) /\ exists fs_q_dst_natural_step_prefix_body_start. fs_u_dst_natural_step_prefix = fs_q_dst_natural_step_prefix_body_start * S ((S (0)) * fs_v_dst_natural_step_prefix) + (0))) /\ ((((exists fs_h_dst_natural_step_prefix_body_terminal. fs_h_dst_natural_step_prefix_body_terminal + S (r) = S ((S (l)) * fs_v_dst_natural_step_prefix)) /\ exists fs_q_dst_natural_step_prefix_body_terminal. fs_u_dst_natural_step_prefix = fs_q_dst_natural_step_prefix_body_terminal * S ((S (l)) * fs_v_dst_natural_step_prefix) + (r))) /\ forall fs_i_dst_natural_step_prefix_body_steps. (exists fs_lt_dst_natural_step_prefix_body_steps_bound. fs_lt_dst_natural_step_prefix_body_steps_bound + S fs_i_dst_natural_step_prefix_body_steps = l) -> exists fs_a_dst_natural_step_prefix_body_steps fs_r_dst_natural_step_prefix_body_steps fs_s_dst_natural_step_prefix_body_steps. ((((exists fs_h_dst_natural_step_prefix_body_steps_summand. fs_h_dst_natural_step_prefix_body_steps_summand + S (fs_a_dst_natural_step_prefix_body_steps) = S ((S (fs_i_dst_natural_step_prefix_body_steps)) * c)) /\ exists fs_q_dst_natural_step_prefix_body_steps_summand. b = fs_q_dst_natural_step_prefix_body_steps_summand * S ((S (fs_i_dst_natural_step_prefix_body_steps)) * c) + (fs_a_dst_natural_step_prefix_body_steps))) /\ ((((exists fs_h_dst_natural_step_prefix_body_steps_partial. fs_h_dst_natural_step_prefix_body_steps_partial + S (fs_r_dst_natural_step_prefix_body_steps) = S ((S (fs_i_dst_natural_step_prefix_body_steps)) * fs_v_dst_natural_step_prefix)) /\ exists fs_q_dst_natural_step_prefix_body_steps_partial. fs_u_dst_natural_step_prefix = fs_q_dst_natural_step_prefix_body_steps_partial * S ((S (fs_i_dst_natural_step_prefix_body_steps)) * fs_v_dst_natural_step_prefix) + (fs_r_dst_natural_step_prefix_body_steps))) /\ ((((exists fs_h_dst_natural_step_prefix_body_steps_successor. fs_h_dst_natural_step_prefix_body_steps_successor + S (fs_s_dst_natural_step_prefix_body_steps) = S ((S (S fs_i_dst_natural_step_prefix_body_steps)) * fs_v_dst_natural_step_prefix)) /\ exists fs_q_dst_natural_step_prefix_body_steps_successor. fs_u_dst_natural_step_prefix = fs_q_dst_natural_step_prefix_body_steps_successor * S ((S (S fs_i_dst_natural_step_prefix_body_steps)) * fs_v_dst_natural_step_prefix) + (fs_s_dst_natural_step_prefix_body_steps))) /\ fs_s_dst_natural_step_prefix_body_steps = fs_r_dst_natural_step_prefix_body_steps + fs_a_dst_natural_step_prefix_body_steps)))))) -> (((exists ff_h_pvs_natural_step_last. ff_h_pvs_natural_step_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_pvs_natural_step_last. b = ff_q_pvs_natural_step_last * S ((S (l)) * c) + (a))) -> (exists fs_u_dst_natural_step_result fs_v_dst_natural_step_result. ((((exists fs_h_dst_natural_step_result_body_start. fs_h_dst_natural_step_result_body_start + S (0) = S ((S (0)) * fs_v_dst_natural_step_result)) /\ exists fs_q_dst_natural_step_result_body_start. fs_u_dst_natural_step_result = fs_q_dst_natural_step_result_body_start * S ((S (0)) * fs_v_dst_natural_step_result) + (0))) /\ ((((exists fs_h_dst_natural_step_result_body_terminal. fs_h_dst_natural_step_result_body_terminal + S (r + a) = S ((S (S l)) * fs_v_dst_natural_step_result)) /\ exists fs_q_dst_natural_step_result_body_terminal. fs_u_dst_natural_step_result = fs_q_dst_natural_step_result_body_terminal * S ((S (S l)) * fs_v_dst_natural_step_result) + (r + a))) /\ forall fs_i_dst_natural_step_result_body_steps. (exists fs_lt_dst_natural_step_result_body_steps_bound. fs_lt_dst_natural_step_result_body_steps_bound + S fs_i_dst_natural_step_result_body_steps = S l) -> exists fs_a_dst_natural_step_result_body_steps fs_r_dst_natural_step_result_body_steps fs_s_dst_natural_step_result_body_steps. ((((exists fs_h_dst_natural_step_result_body_steps_summand. fs_h_dst_natural_step_result_body_steps_summand + S (fs_a_dst_natural_step_result_body_steps) = S ((S (fs_i_dst_natural_step_result_body_steps)) * c)) /\ exists fs_q_dst_natural_step_result_body_steps_summand. b = fs_q_dst_natural_step_result_body_steps_summand * S ((S (fs_i_dst_natural_step_result_body_steps)) * c) + (fs_a_dst_natural_step_result_body_steps))) /\ ((((exists fs_h_dst_natural_step_result_body_steps_partial. fs_h_dst_natural_step_result_body_steps_partial + S (fs_r_dst_natural_step_result_body_steps) = S ((S (fs_i_dst_natural_step_result_body_steps)) * fs_v_dst_natural_step_result)) /\ exists fs_q_dst_natural_step_result_body_steps_partial. fs_u_dst_natural_step_result = fs_q_dst_natural_step_result_body_steps_partial * S ((S (fs_i_dst_natural_step_result_body_steps)) * fs_v_dst_natural_step_result) + (fs_r_dst_natural_step_result_body_steps))) /\ ((((exists fs_h_dst_natural_step_result_body_steps_successor. fs_h_dst_natural_step_result_body_steps_successor + S (fs_s_dst_natural_step_result_body_steps) = S ((S (S fs_i_dst_natural_step_result_body_steps)) * fs_v_dst_natural_step_result)) /\ exists fs_q_dst_natural_step_result_body_steps_successor. fs_u_dst_natural_step_result = fs_q_dst_natural_step_result_body_steps_successor * S ((S (S fs_i_dst_natural_step_result_body_steps)) * fs_v_dst_natural_step_result) + (fs_s_dst_natural_step_result_body_steps))) /\ fs_s_dst_natural_step_result_body_steps = fs_r_dst_natural_step_result_body_steps + fs_a_dst_natural_step_result_body_steps))))))

Complete tactic proof in conservative notation

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

51 script commands · 8 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–7

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 r
  5. L5
    intro a
  6. L6
    intro hs
  7. L7
    intro ha
02Establish htL8–12

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

  1. L8
    have ht : ∃ t. Sum(b,c,S l,t)Definitions: Sum(b,c,S l,t)Original native command in the exact edition
  2. L9
    specialize beta_sum_exists (b)
  3. L10
    specialize beta_sum_exists (c)
  4. L11
    specialize beta_sum_exists (S l)
  5. L12
    apply beta_sum_exists
03Separate the logical casesL13–13

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

  1. L13
    cases ht
04Establish hdL14–20

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

  1. L14
    have hd : ∃ dsa_summand_natural_step_decomp. ∃ dsa_partial_natural_step_decomp. BetaAt(b,c,l,dsa_summand_natural_step_decomp) ∧ (Sum(b,c,l,dsa_partial_natural_step_decomp) ∧ x = dsa_partial_natural_step_decomp + dsa_summand_natural_step_decomp)Definitions: BetaAt(b,c,l,dsa_summand_natural_step_decomp)Sum(b,c,l,dsa_partial_natural_step_decomp)Original native command in the exact edition
  2. L15
    specialize beta_sum_succ_decompose (b)
  3. L16
    specialize beta_sum_succ_decompose (c)
  4. L17
    specialize beta_sum_succ_decompose (l)
  5. L18
    specialize beta_sum_succ_decompose (x)
  6. L19
    apply beta_sum_succ_decompose
  7. L20
    exact ht_witness
05Separate the logical casesL21–24

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

  1. L21
    cases hd
  2. L22
    cases hd_witness
  3. L23
    cases hd_witness_witness
  4. L24
    cases hd_witness_witness_right
06Establish heqaL25–33

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

  1. L25
    have heqa : x1 = a
  2. L26
    specialize beta_at_unique (b)
  3. L27
    specialize beta_at_unique (c)
  4. L28
    specialize beta_at_unique (l)
  5. L29
    specialize beta_at_unique (x1)
  6. L30
    specialize beta_at_unique (a)
  7. L31
    apply beta_at_unique
  8. L32
    exact hd_witness_witness_left
  9. L33
    exact ha
07Establish heqrL34–42

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

  1. L34
    have heqr : x2 = r
  2. L35
    specialize beta_sum_functional (b)
  3. L36
    specialize beta_sum_functional (c)
  4. L37
    specialize beta_sum_functional (l)
  5. L38
    specialize beta_sum_functional (x2)
  6. L39
    specialize beta_sum_functional (r)
  7. L40
    apply beta_sum_functional
  8. L41
    exact hd_witness_witness_right_left
  9. L42
    exact hs
08Establish heqL43–51

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

  1. L43
    have heq : x = r + a
  2. L44
    trans x2 + x1
  3. L45
    exact hd_witness_witness_right_right
  4. L46
    rewrite heqr
  5. L47
    rewrite heqa
  6. L48
    refl
  7. L49
    rewrite heq at ht_witness
  8. L50
    rewrite heq at ht_witness
  9. L51
    exact ht_witness

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro r
  5. 0005intro a
  6. 0006intro hs
  7. 0007intro ha
  8. 0008have ht : ∃ t. Sum(b,c,S l,t)
  9. 0009specialize beta_sum_exists (b)
  10. 0010specialize beta_sum_exists (c)
  11. 0011specialize beta_sum_exists (S l)
  12. 0012apply beta_sum_exists
  13. 0013cases ht
  14. 0014have hd : ∃ dsa_summand_natural_step_decomp. ∃ dsa_partial_natural_step_decomp. BetaAt(b,c,l,dsa_summand_natural_step_decomp) ∧ (Sum(b,c,l,dsa_partial_natural_step_decomp) ∧ x = dsa_partial_natural_step_decomp + dsa_summand_natural_step_decomp)
  15. 0015specialize beta_sum_succ_decompose (b)
  16. 0016specialize beta_sum_succ_decompose (c)
  17. 0017specialize beta_sum_succ_decompose (l)
  18. 0018specialize beta_sum_succ_decompose (x)
  19. 0019apply beta_sum_succ_decompose
  20. 0020exact ht_witness
  21. 0021cases hd
  22. 0022cases hd_witness
  23. 0023cases hd_witness_witness
  24. 0024cases hd_witness_witness_right
  25. 0025have heqa : x1 = a
  26. 0026specialize beta_at_unique (b)
  27. 0027specialize beta_at_unique (c)
  28. 0028specialize beta_at_unique (l)
  29. 0029specialize beta_at_unique (x1)
  30. 0030specialize beta_at_unique (a)
  31. 0031apply beta_at_unique
  32. 0032exact hd_witness_witness_left
  33. 0033exact ha
  34. 0034have heqr : x2 = r
  35. 0035specialize beta_sum_functional (b)
  36. 0036specialize beta_sum_functional (c)
  37. 0037specialize beta_sum_functional (l)
  38. 0038specialize beta_sum_functional (x2)
  39. 0039specialize beta_sum_functional (r)
  40. 0040apply beta_sum_functional
  41. 0041exact hd_witness_witness_right_left
  42. 0042exact hs
  43. 0043have heq : x = r + a
  44. 0044trans x2 + x1
  45. 0045exact hd_witness_witness_right_right
  46. 0046rewrite heqr
  47. 0047rewrite heqa
  48. 0048refl
  49. 0049rewrite heq at ht_witness
  50. 0050rewrite heq at ht_witness
  51. 0051exact ht_witness