PC000A

beta_sum_entry_le

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

Every actual nonnegative summand is at most its actual finite sum.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall b c l n i a. (exists fs_u_pc_entry_le_sum fs_v_pc_entry_le_sum. ((((exists fs_h_pc_entry_le_sum_body_start. fs_h_pc_entry_le_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_entry_le_sum)) /\ exists fs_q_pc_entry_le_sum_body_start. fs_u_pc_entry_le_sum = fs_q_pc_entry_le_sum_body_start * S ((S (0)) * fs_v_pc_entry_le_sum) + (0))) /\ ((((exists fs_h_pc_entry_le_sum_body_terminal. fs_h_pc_entry_le_sum_body_terminal + S (n) = S ((S (l)) * fs_v_pc_entry_le_sum)) /\ exists fs_q_pc_entry_le_sum_body_terminal. fs_u_pc_entry_le_sum = fs_q_pc_entry_le_sum_body_terminal * S ((S (l)) * fs_v_pc_entry_le_sum) + (n))) /\ forall fs_i_pc_entry_le_sum_body_steps. (exists fs_lt_pc_entry_le_sum_body_steps_bound. fs_lt_pc_entry_le_sum_body_steps_bound + S fs_i_pc_entry_le_sum_body_steps = l) -> exists fs_a_pc_entry_le_sum_body_steps fs_r_pc_entry_le_sum_body_steps fs_s_pc_entry_le_sum_body_steps. ((((exists fs_h_pc_entry_le_sum_body_steps_summand. fs_h_pc_entry_le_sum_body_steps_summand + S (fs_a_pc_entry_le_sum_body_steps) = S ((S (fs_i_pc_entry_le_sum_body_steps)) * c)) /\ exists fs_q_pc_entry_le_sum_body_steps_summand. b = fs_q_pc_entry_le_sum_body_steps_summand * S ((S (fs_i_pc_entry_le_sum_body_steps)) * c) + (fs_a_pc_entry_le_sum_body_steps))) /\ ((((exists fs_h_pc_entry_le_sum_body_steps_partial. fs_h_pc_entry_le_sum_body_steps_partial + S (fs_r_pc_entry_le_sum_body_steps) = S ((S (fs_i_pc_entry_le_sum_body_steps)) * fs_v_pc_entry_le_sum)) /\ exists fs_q_pc_entry_le_sum_body_steps_partial. fs_u_pc_entry_le_sum = fs_q_pc_entry_le_sum_body_steps_partial * S ((S (fs_i_pc_entry_le_sum_body_steps)) * fs_v_pc_entry_le_sum) + (fs_r_pc_entry_le_sum_body_steps))) /\ ((((exists fs_h_pc_entry_le_sum_body_steps_successor. fs_h_pc_entry_le_sum_body_steps_successor + S (fs_s_pc_entry_le_sum_body_steps) = S ((S (S fs_i_pc_entry_le_sum_body_steps)) * fs_v_pc_entry_le_sum)) /\ exists fs_q_pc_entry_le_sum_body_steps_successor. fs_u_pc_entry_le_sum = fs_q_pc_entry_le_sum_body_steps_successor * S ((S (S fs_i_pc_entry_le_sum_body_steps)) * fs_v_pc_entry_le_sum) + (fs_s_pc_entry_le_sum_body_steps))) /\ fs_s_pc_entry_le_sum_body_steps = fs_r_pc_entry_le_sum_body_steps + fs_a_pc_entry_le_sum_body_steps)))))) -> (exists pc_lt_entry_le_index. pc_lt_entry_le_index + S (i) = (l)) -> (((exists fs_h_pc_entry_le_value. fs_h_pc_entry_le_value + S (a) = S ((S (i)) * c)) /\ exists fs_q_pc_entry_le_value. b = fs_q_pc_entry_le_value * S ((S (i)) * c) + (a))) -> (exists pc_le_entry_le_result. pc_le_entry_le_result + (a) = (n))

Constructive proof overview

Generated structural guide

Every actual nonnegative summand is at most its actual finite sum.

The unchanged tactic script uses 9 declared prerequisites and contains 73 exact native proof lines.

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

Proof neighborhood

Direct dependencies

lt_not_le Stable theorem; checked-use authorized zero_le Stable theorem; checked-use authorized beta_sum_succ_decompose Stable theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized le_add_left Stable theorem; checked-use authorized le_add_right Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized

Direct dependents

PC000B prime_count_positive_above_one

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

73 script commands · 16 reading checkpoints · 3 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–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–9

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

  1. L3
    induction l
  2. L4
    intro n
  3. L5
    intro i
  4. L6
    intro a
  5. L7
    intro hs
  6. L8
    intro hi
  7. L9
    intro ha
03Separate the logical casesL10–10

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

  1. L10
    exfalso
04Use earlier factsL11–16

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

  1. L11
    specialize lt_not_le i
  2. L12
    specialize lt_not_le 0
  3. L13
    apply lt_not_le
  4. L14
    exact hi
  5. L15
    specialize zero_le i
  6. L16
    apply zero_le
05Fix variables and assumptionsL17–22

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

  1. L17
    intro n
  2. L18
    intro i
  3. L19
    intro a
  4. L20
    intro hs
  5. L21
    intro hi
  6. L22
    intro ha
06Establish hdL23–29

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

  1. L23
    have hd : ∃ v. ∃ w. BetaAt(b,c,l,v) ∧ (Sum(b,c,l,w) ∧ n = w + v)Definitions: BetaAtSum
  2. L24
    specialize beta_sum_succ_decompose b
  3. L25
    specialize beta_sum_succ_decompose c
  4. L26
    specialize beta_sum_succ_decompose l
  5. L27
    specialize beta_sum_succ_decompose n
  6. L28
    apply beta_sum_succ_decompose
  7. L29
    exact hs
07Separate the logical casesL30–33

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

  1. L30
    cases hd
  2. L31
    cases hd_witness
  3. L32
    cases hd_witness_witness
  4. L33
    cases hd_witness_witness_right
08Establish hcL34–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L34
    have hc : i = l \/ exists g. g + S i = l
  2. L35
    specialize le_eq_or_lt i
  3. L36
    specialize le_eq_or_lt l
  4. L37
    apply le_eq_or_lt
  5. L38
    specialize le_of_succ_le_succ i
  6. L39
    specialize le_of_succ_le_succ l
  7. L40
    apply le_of_succ_le_succ
  8. L41
    exact hi
09Separate the logical casesL42–42

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

  1. L42
    cases hc
10Calculate and transport equalitiesL43–44

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

  1. L43
    rewrite hc_left at ha
  2. L44
    rewrite hc_left at ha
11Establish heqL45–54

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

  1. L45
    have heq : a = x
  2. L46
    specialize beta_at_unique b
  3. L47
    specialize beta_at_unique c
  4. L48
    specialize beta_at_unique l
  5. L49
    specialize beta_at_unique a
  6. L50
    specialize beta_at_unique x
  7. L51
    apply beta_at_unique
  8. L52
    exact ha
  9. L53
    exact hd_witness_witness_left
  10. L54
    rewrite heq
12Calculate and transport equalitiesL55–55

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

  1. L55
    rewrite hd_witness_witness_right_right
13Use earlier factsL56–65

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

  1. L56
    specialize le_add_left x
  2. L57
    specialize le_add_left x1
  3. L58
    apply le_add_left
  4. L59
    specialize le_trans a
  5. L60
    specialize le_trans x1
  6. L61
    specialize le_trans n
  7. L62
    apply le_trans
  8. L63
    specialize IH x1
  9. L64
    specialize IH i
  10. L65
    specialize IH a
14Use earlier factsL66–69

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

  1. L66
    apply IH
  2. L67
    exact hd_witness_witness_right_left
  3. L68
    exact hc_right
  4. L69
    exact ha
15Calculate and transport equalitiesL70–70

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

  1. L70
    rewrite hd_witness_witness_right_right
16Use earlier factsL71–73

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

  1. L71
    specialize le_add_right x1
  2. L72
    specialize le_add_right x
  3. L73
    apply le_add_right

Library-wide reading audit

Original exact command ledger · 73 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro n
  5. 0005intro i
  6. 0006intro a
  7. 0007intro hs
  8. 0008intro hi
  9. 0009intro ha
  10. 0010exfalso
  11. 0011specialize lt_not_le i
  12. 0012specialize lt_not_le 0
  13. 0013apply lt_not_le
  14. 0014exact hi
  15. 0015specialize zero_le i
  16. 0016apply zero_le
  17. 0017intro n
  18. 0018intro i
  19. 0019intro a
  20. 0020intro hs
  21. 0021intro hi
  22. 0022intro ha
  23. 0023have hd : exists v w. (((exists fs_h_pc_entry_le_last. fs_h_pc_entry_le_last + S (v) = S ((S (l)) * c)) /\ exists fs_q_pc_entry_le_last. b = fs_q_pc_entry_le_last * S ((S (l)) * c) + (v))) /\ ((exists fs_u_pc_entry_le_prefix fs_v_pc_entry_le_prefix. ((((exists fs_h_pc_entry_le_prefix_body_start. fs_h_pc_entry_le_prefix_body_start + S (0) = S ((S (0)) * fs_v_pc_entry_le_prefix)) /\ exists fs_q_pc_entry_le_prefix_body_start. fs_u_pc_entry_le_prefix = fs_q_pc_entry_le_prefix_body_start * S ((S (0)) * fs_v_pc_entry_le_prefix) + (0))) /\ ((((exists fs_h_pc_entry_le_prefix_body_terminal. fs_h_pc_entry_le_prefix_body_terminal + S (w) = S ((S (l)) * fs_v_pc_entry_le_prefix)) /\ exists fs_q_pc_entry_le_prefix_body_terminal. fs_u_pc_entry_le_prefix = fs_q_pc_entry_le_prefix_body_terminal * S ((S (l)) * fs_v_pc_entry_le_prefix) + (w))) /\ forall fs_i_pc_entry_le_prefix_body_steps. (exists fs_lt_pc_entry_le_prefix_body_steps_bound. fs_lt_pc_entry_le_prefix_body_steps_bound + S fs_i_pc_entry_le_prefix_body_steps = l) -> exists fs_a_pc_entry_le_prefix_body_steps fs_r_pc_entry_le_prefix_body_steps fs_s_pc_entry_le_prefix_body_steps. ((((exists fs_h_pc_entry_le_prefix_body_steps_summand. fs_h_pc_entry_le_prefix_body_steps_summand + S (fs_a_pc_entry_le_prefix_body_steps) = S ((S (fs_i_pc_entry_le_prefix_body_steps)) * c)) /\ exists fs_q_pc_entry_le_prefix_body_steps_summand. b = fs_q_pc_entry_le_prefix_body_steps_summand * S ((S (fs_i_pc_entry_le_prefix_body_steps)) * c) + (fs_a_pc_entry_le_prefix_body_steps))) /\ ((((exists fs_h_pc_entry_le_prefix_body_steps_partial. fs_h_pc_entry_le_prefix_body_steps_partial + S (fs_r_pc_entry_le_prefix_body_steps) = S ((S (fs_i_pc_entry_le_prefix_body_steps)) * fs_v_pc_entry_le_prefix)) /\ exists fs_q_pc_entry_le_prefix_body_steps_partial. fs_u_pc_entry_le_prefix = fs_q_pc_entry_le_prefix_body_steps_partial * S ((S (fs_i_pc_entry_le_prefix_body_steps)) * fs_v_pc_entry_le_prefix) + (fs_r_pc_entry_le_prefix_body_steps))) /\ ((((exists fs_h_pc_entry_le_prefix_body_steps_successor. fs_h_pc_entry_le_prefix_body_steps_successor + S (fs_s_pc_entry_le_prefix_body_steps) = S ((S (S fs_i_pc_entry_le_prefix_body_steps)) * fs_v_pc_entry_le_prefix)) /\ exists fs_q_pc_entry_le_prefix_body_steps_successor. fs_u_pc_entry_le_prefix = fs_q_pc_entry_le_prefix_body_steps_successor * S ((S (S fs_i_pc_entry_le_prefix_body_steps)) * fs_v_pc_entry_le_prefix) + (fs_s_pc_entry_le_prefix_body_steps))) /\ fs_s_pc_entry_le_prefix_body_steps = fs_r_pc_entry_le_prefix_body_steps + fs_a_pc_entry_le_prefix_body_steps)))))) /\ n = w + v)
  24. 0024specialize beta_sum_succ_decompose b
  25. 0025specialize beta_sum_succ_decompose c
  26. 0026specialize beta_sum_succ_decompose l
  27. 0027specialize beta_sum_succ_decompose n
  28. 0028apply beta_sum_succ_decompose
  29. 0029exact hs
  30. 0030cases hd
  31. 0031cases hd_witness
  32. 0032cases hd_witness_witness
  33. 0033cases hd_witness_witness_right
  34. 0034have hc : i = l \/ exists g. g + S i = l
  35. 0035specialize le_eq_or_lt i
  36. 0036specialize le_eq_or_lt l
  37. 0037apply le_eq_or_lt
  38. 0038specialize le_of_succ_le_succ i
  39. 0039specialize le_of_succ_le_succ l
  40. 0040apply le_of_succ_le_succ
  41. 0041exact hi
  42. 0042cases hc
  43. 0043rewrite hc_left at ha
  44. 0044rewrite hc_left at ha
  45. 0045have heq : a = x
  46. 0046specialize beta_at_unique b
  47. 0047specialize beta_at_unique c
  48. 0048specialize beta_at_unique l
  49. 0049specialize beta_at_unique a
  50. 0050specialize beta_at_unique x
  51. 0051apply beta_at_unique
  52. 0052exact ha
  53. 0053exact hd_witness_witness_left
  54. 0054rewrite heq
  55. 0055rewrite hd_witness_witness_right_right
  56. 0056specialize le_add_left x
  57. 0057specialize le_add_left x1
  58. 0058apply le_add_left
  59. 0059specialize le_trans a
  60. 0060specialize le_trans x1
  61. 0061specialize le_trans n
  62. 0062apply le_trans
  63. 0063specialize IH x1
  64. 0064specialize IH i
  65. 0065specialize IH a
  66. 0066apply IH
  67. 0067exact hd_witness_witness_right_left
  68. 0068exact hc_right
  69. 0069exact ha
  70. 0070rewrite hd_witness_witness_right_right
  71. 0071specialize le_add_right x1
  72. 0072specialize le_add_right x
  73. 0073apply le_add_right