PC000A

beta_sum_entry_le

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

Alpha v34 checked-use · first admitted v27 · 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. Exact original first-admission records.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ n. ∀ i. ∀ a. Sum(b,c,l,n) → Lt(i,l) → BetaAt(b,c,i,a) → Le(a,n)

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

Definition DAG

Le(a,b) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 2Sum(b,c,l,z) · 2

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisitebeta_sum_succ_decompose · checked external prerequisitele_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisitebeta_at_unique · checked external prerequisitele_add_left · checked external prerequisitele_add_right · checked external prerequisitele_trans · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

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

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.

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–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: BetaAt(b,c,l,v)Sum(b,c,l,w)Original native command in the exact edition
  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 ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  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 defined 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 : ∃ v. ∃ w. BetaAt(b,c,l,v) ∧ (Sum(b,c,l,w) ∧ 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 ∨ Lt(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