SS0012

divisor_natural_sum_successor_intro

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

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

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 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))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 51 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_sum_exists Stable theorem; checked-use authorized beta_sum_succ_decompose Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized beta_sum_functional Stable theorem; checked-use authorized

Direct dependents

SS0016 divisor_signed_sum_successor_intro

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

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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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: BetaAtSum
  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 exact 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 : exists t. (exists fs_u_dst_natural_step_exists fs_v_dst_natural_step_exists. ((((exists fs_h_dst_natural_step_exists_body_start. fs_h_dst_natural_step_exists_body_start + S (0) = S ((S (0)) * fs_v_dst_natural_step_exists)) /\ exists fs_q_dst_natural_step_exists_body_start. fs_u_dst_natural_step_exists = fs_q_dst_natural_step_exists_body_start * S ((S (0)) * fs_v_dst_natural_step_exists) + (0))) /\ ((((exists fs_h_dst_natural_step_exists_body_terminal. fs_h_dst_natural_step_exists_body_terminal + S (t) = S ((S (S l)) * fs_v_dst_natural_step_exists)) /\ exists fs_q_dst_natural_step_exists_body_terminal. fs_u_dst_natural_step_exists = fs_q_dst_natural_step_exists_body_terminal * S ((S (S l)) * fs_v_dst_natural_step_exists) + (t))) /\ forall fs_i_dst_natural_step_exists_body_steps. (exists fs_lt_dst_natural_step_exists_body_steps_bound. fs_lt_dst_natural_step_exists_body_steps_bound + S fs_i_dst_natural_step_exists_body_steps = S l) -> exists fs_a_dst_natural_step_exists_body_steps fs_r_dst_natural_step_exists_body_steps fs_s_dst_natural_step_exists_body_steps. ((((exists fs_h_dst_natural_step_exists_body_steps_summand. fs_h_dst_natural_step_exists_body_steps_summand + S (fs_a_dst_natural_step_exists_body_steps) = S ((S (fs_i_dst_natural_step_exists_body_steps)) * c)) /\ exists fs_q_dst_natural_step_exists_body_steps_summand. b = fs_q_dst_natural_step_exists_body_steps_summand * S ((S (fs_i_dst_natural_step_exists_body_steps)) * c) + (fs_a_dst_natural_step_exists_body_steps))) /\ ((((exists fs_h_dst_natural_step_exists_body_steps_partial. fs_h_dst_natural_step_exists_body_steps_partial + S (fs_r_dst_natural_step_exists_body_steps) = S ((S (fs_i_dst_natural_step_exists_body_steps)) * fs_v_dst_natural_step_exists)) /\ exists fs_q_dst_natural_step_exists_body_steps_partial. fs_u_dst_natural_step_exists = fs_q_dst_natural_step_exists_body_steps_partial * S ((S (fs_i_dst_natural_step_exists_body_steps)) * fs_v_dst_natural_step_exists) + (fs_r_dst_natural_step_exists_body_steps))) /\ ((((exists fs_h_dst_natural_step_exists_body_steps_successor. fs_h_dst_natural_step_exists_body_steps_successor + S (fs_s_dst_natural_step_exists_body_steps) = S ((S (S fs_i_dst_natural_step_exists_body_steps)) * fs_v_dst_natural_step_exists)) /\ exists fs_q_dst_natural_step_exists_body_steps_successor. fs_u_dst_natural_step_exists = fs_q_dst_natural_step_exists_body_steps_successor * S ((S (S fs_i_dst_natural_step_exists_body_steps)) * fs_v_dst_natural_step_exists) + (fs_s_dst_natural_step_exists_body_steps))) /\ fs_s_dst_natural_step_exists_body_steps = fs_r_dst_natural_step_exists_body_steps + fs_a_dst_natural_step_exists_body_steps))))))
  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 : exists dsa_summand_natural_step_decomp dsa_partial_natural_step_decomp. ((((exists ff_h_pvs_natural_step_decomplast. ff_h_pvs_natural_step_decomplast + S (dsa_summand_natural_step_decomp) = S ((S (l)) * c)) /\ exists ff_q_pvs_natural_step_decomplast. b = ff_q_pvs_natural_step_decomplast * S ((S (l)) * c) + (dsa_summand_natural_step_decomp))) /\ (((exists fs_u_dst_natural_step_decompprefix fs_v_dst_natural_step_decompprefix. ((((exists fs_h_dst_natural_step_decompprefix_body_start. fs_h_dst_natural_step_decompprefix_body_start + S (0) = S ((S (0)) * fs_v_dst_natural_step_decompprefix)) /\ exists fs_q_dst_natural_step_decompprefix_body_start. fs_u_dst_natural_step_decompprefix = fs_q_dst_natural_step_decompprefix_body_start * S ((S (0)) * fs_v_dst_natural_step_decompprefix) + (0))) /\ ((((exists fs_h_dst_natural_step_decompprefix_body_terminal. fs_h_dst_natural_step_decompprefix_body_terminal + S (dsa_partial_natural_step_decomp) = S ((S (l)) * fs_v_dst_natural_step_decompprefix)) /\ exists fs_q_dst_natural_step_decompprefix_body_terminal. fs_u_dst_natural_step_decompprefix = fs_q_dst_natural_step_decompprefix_body_terminal * S ((S (l)) * fs_v_dst_natural_step_decompprefix) + (dsa_partial_natural_step_decomp))) /\ forall fs_i_dst_natural_step_decompprefix_body_steps. (exists fs_lt_dst_natural_step_decompprefix_body_steps_bound. fs_lt_dst_natural_step_decompprefix_body_steps_bound + S fs_i_dst_natural_step_decompprefix_body_steps = l) -> exists fs_a_dst_natural_step_decompprefix_body_steps fs_r_dst_natural_step_decompprefix_body_steps fs_s_dst_natural_step_decompprefix_body_steps. ((((exists fs_h_dst_natural_step_decompprefix_body_steps_summand. fs_h_dst_natural_step_decompprefix_body_steps_summand + S (fs_a_dst_natural_step_decompprefix_body_steps) = S ((S (fs_i_dst_natural_step_decompprefix_body_steps)) * c)) /\ exists fs_q_dst_natural_step_decompprefix_body_steps_summand. b = fs_q_dst_natural_step_decompprefix_body_steps_summand * S ((S (fs_i_dst_natural_step_decompprefix_body_steps)) * c) + (fs_a_dst_natural_step_decompprefix_body_steps))) /\ ((((exists fs_h_dst_natural_step_decompprefix_body_steps_partial. fs_h_dst_natural_step_decompprefix_body_steps_partial + S (fs_r_dst_natural_step_decompprefix_body_steps) = S ((S (fs_i_dst_natural_step_decompprefix_body_steps)) * fs_v_dst_natural_step_decompprefix)) /\ exists fs_q_dst_natural_step_decompprefix_body_steps_partial. fs_u_dst_natural_step_decompprefix = fs_q_dst_natural_step_decompprefix_body_steps_partial * S ((S (fs_i_dst_natural_step_decompprefix_body_steps)) * fs_v_dst_natural_step_decompprefix) + (fs_r_dst_natural_step_decompprefix_body_steps))) /\ ((((exists fs_h_dst_natural_step_decompprefix_body_steps_successor. fs_h_dst_natural_step_decompprefix_body_steps_successor + S (fs_s_dst_natural_step_decompprefix_body_steps) = S ((S (S fs_i_dst_natural_step_decompprefix_body_steps)) * fs_v_dst_natural_step_decompprefix)) /\ exists fs_q_dst_natural_step_decompprefix_body_steps_successor. fs_u_dst_natural_step_decompprefix = fs_q_dst_natural_step_decompprefix_body_steps_successor * S ((S (S fs_i_dst_natural_step_decompprefix_body_steps)) * fs_v_dst_natural_step_decompprefix) + (fs_s_dst_natural_step_decompprefix_body_steps))) /\ fs_s_dst_natural_step_decompprefix_body_steps = fs_r_dst_natural_step_decompprefix_body_steps + fs_a_dst_natural_step_decompprefix_body_steps)))))) /\ ((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