CD0009

finite_sum_entry_le

Every genuinely decoded summand is bounded by the exact finite sum containing it.

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.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

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

beta_sum_succ_decompose · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisitele_add_left · checked external prerequisitele_add_right · checked external prerequisitele_trans · checked external prerequisiteadd_eq_zero_right · checked external prerequisitesucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall b c l n i a. (exists ff_u_fms_sum ff_v_fms_sum. ((((exists ff_h_fms_sum_start. ff_h_fms_sum_start + S (0) = S ((S (0)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_start. ff_u_fms_sum = ff_q_fms_sum_start * S ((S (0)) * ff_v_fms_sum) + (0))) /\ ((((exists ff_h_fms_sum_terminal. ff_h_fms_sum_terminal + S ((n)) = S ((S ((l))) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_terminal. ff_u_fms_sum = ff_q_fms_sum_terminal * S ((S ((l))) * ff_v_fms_sum) + ((n)))) /\ forall ff_i_fms_sum. (exists ff_lt_fms_sum_bound. ff_lt_fms_sum_bound + S ff_i_fms_sum = (l)) -> exists ff_a_fms_sum ff_r_fms_sum ff_s_fms_sum. ((((exists ff_h_fms_sum_summand. ff_h_fms_sum_summand + S (ff_a_fms_sum) = S ((S (ff_i_fms_sum)) * (c))) /\ exists ff_q_fms_sum_summand. (b) = ff_q_fms_sum_summand * S ((S (ff_i_fms_sum)) * (c)) + (ff_a_fms_sum))) /\ ((((exists ff_h_fms_sum_partial. ff_h_fms_sum_partial + S (ff_r_fms_sum) = S ((S (ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_partial. ff_u_fms_sum = ff_q_fms_sum_partial * S ((S (ff_i_fms_sum)) * ff_v_fms_sum) + (ff_r_fms_sum))) /\ ((((exists ff_h_fms_sum_successor. ff_h_fms_sum_successor + S (ff_s_fms_sum) = S ((S (S ff_i_fms_sum)) * ff_v_fms_sum)) /\ exists ff_q_fms_sum_successor. ff_u_fms_sum = ff_q_fms_sum_successor * S ((S (S ff_i_fms_sum)) * ff_v_fms_sum) + (ff_s_fms_sum))) /\ ff_s_fms_sum = ff_r_fms_sum + ff_a_fms_sum)))))) -> (exists fms_gap_lt. fms_gap_lt + S (i) = (l)) -> (((exists fs_h_fms_entry_le. fs_h_fms_entry_le + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_entry_le. b = fs_q_fms_entry_le * S ((S (i)) * c) + (a))) -> (exists fms_gap_le. fms_gap_le + (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 · 4 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 hsum
  6. L8
    intro hi
  7. L9
    intro ha
03Separate the logical casesL10–11

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

  1. L10
    exfalso
  2. L11
    cases hi
04Establish hzL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L12
    have hz : S i=0
  2. L13
    specialize add_eq_zero_right x
  3. L14
    specialize add_eq_zero_right S i
  4. L15
    apply add_eq_zero_right
  5. L16
    exact hi_witness
  6. L17
    specialize succ_ne_zero i
  7. L18
    apply succ_ne_zero
  8. L19
    exact hz
  9. L20
    intro n
  10. L21
    intro i
05Fix variables and assumptionsL22–25

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

  1. L22
    intro a
  2. L23
    intro hsum
  3. L24
    intro hi
  4. L25
    intro ha
06Establish hdL26–32

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

  1. L26
    have hd : ∃ fms_term_hd. ∃ fms_sum_hd. BetaAt(b,c,l,fms_term_hd) ∧ (Sum(b,c,l,fms_sum_hd) ∧ n = fms_sum_hd + fms_term_hd)Definitions: BetaAt(b,c,l,fms_term_hd)Sum(b,c,l,fms_sum_hd)Original native command in the exact edition
  2. L27
    specialize beta_sum_succ_decompose b
  3. L28
    specialize beta_sum_succ_decompose c
  4. L29
    specialize beta_sum_succ_decompose l
  5. L30
    specialize beta_sum_succ_decompose n
  6. L31
    apply beta_sum_succ_decompose
  7. L32
    exact hsum
07Separate the logical casesL33–36

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

  1. L33
    cases hd
  2. L34
    cases hd_witness
  3. L35
    cases hd_witness_witness
  4. L36
    cases hd_witness_witness_right
08Establish hcaseL37–41

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

  1. L37
    have hcase : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L38
    specialize finite_lt_succ_eq_or_lt l
  3. L39
    specialize finite_lt_succ_eq_or_lt i
  4. L40
    apply finite_lt_succ_eq_or_lt
  5. L41
    exact hi
09Separate the logical casesL42–42

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

  1. L42
    cases hcase
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 hcase_left at ha
  2. L44
    rewrite hcase_left at ha
11Establish heL45–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 he : 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 he
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–58

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
14Calculate and transport equalitiesL59–59

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

  1. L59
    rewrite hd_witness_witness_right_right
15Use earlier factsL60–69

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

  1. L60
    specialize le_trans a
  2. L61
    specialize le_trans x1
  3. L62
    specialize le_trans x1+x
  4. L63
    apply le_trans
  5. L64
    specialize IH x1
  6. L65
    specialize IH i
  7. L66
    specialize IH a
  8. L67
    apply IH
  9. L68
    exact hd_witness_witness_right_left
  10. L69
    exact hcase_right
16Use earlier factsL70–73

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

  1. L70
    exact ha
  2. L71
    specialize le_add_right x1
  3. L72
    specialize le_add_right x
  4. 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 hsum
  8. 0008intro hi
  9. 0009intro ha
  10. 0010exfalso
  11. 0011cases hi
  12. 0012have hz : S i=0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right S i
  15. 0015apply add_eq_zero_right
  16. 0016exact hi_witness
  17. 0017specialize succ_ne_zero i
  18. 0018apply succ_ne_zero
  19. 0019exact hz
  20. 0020intro n
  21. 0021intro i
  22. 0022intro a
  23. 0023intro hsum
  24. 0024intro hi
  25. 0025intro ha
  26. 0026have hd : ∃ fms_term_hd. ∃ fms_sum_hd. BetaAt(b,c,l,fms_term_hd) ∧ (Sum(b,c,l,fms_sum_hd) ∧ n = fms_sum_hd + fms_term_hd)
  27. 0027specialize beta_sum_succ_decompose b
  28. 0028specialize beta_sum_succ_decompose c
  29. 0029specialize beta_sum_succ_decompose l
  30. 0030specialize beta_sum_succ_decompose n
  31. 0031apply beta_sum_succ_decompose
  32. 0032exact hsum
  33. 0033cases hd
  34. 0034cases hd_witness
  35. 0035cases hd_witness_witness
  36. 0036cases hd_witness_witness_right
  37. 0037have hcase : i = l ∨ Lt(i,l)
  38. 0038specialize finite_lt_succ_eq_or_lt l
  39. 0039specialize finite_lt_succ_eq_or_lt i
  40. 0040apply finite_lt_succ_eq_or_lt
  41. 0041exact hi
  42. 0042cases hcase
  43. 0043rewrite hcase_left at ha
  44. 0044rewrite hcase_left at ha
  45. 0045have he : 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 he
  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. 0059rewrite hd_witness_witness_right_right
  60. 0060specialize le_trans a
  61. 0061specialize le_trans x1
  62. 0062specialize le_trans x1+x
  63. 0063apply le_trans
  64. 0064specialize IH x1
  65. 0065specialize IH i
  66. 0066specialize IH a
  67. 0067apply IH
  68. 0068exact hd_witness_witness_right_left
  69. 0069exact hcase_right
  70. 0070exact ha
  71. 0071specialize le_add_right x1
  72. 0072specialize le_add_right x
  73. 0073apply le_add_right