BT00RJ · Bertrand theorem

floor_ceil_division_budget

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Raw canonical division data closes both B6 quotient-budget inequalities.

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.

Statement with defined notation

∀ n. ∀ q. ∀ r. ∀ s. ∀ e. FloorSqrt(2 · n,s) → CeilDivSix(s · s,e) → DivRem(2 · n,3,q,r) → ∃ x. q + x = n ∧ Le(2 · n,6 · x) ∧ (Le(e,x) ∧ Le(q + e,n)) ∧ Lt(r,3)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0007 DivRem PD0051 FloorSqrt PD0052 CeilDivSix

7 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

4 occurrences

Exact expanded native-PA statement
forall n q r s e. (((exists bcs_sqrt_lower_gap_division_bridge_floor. bcs_sqrt_lower_gap_division_bridge_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_division_bridge_floor. bcs_sqrt_upper_gap_division_bridge_floor + S (2 * n) = S (s) * S (s))) -> (((exists bcs_lower_gap_division_bridge_ceil. bcs_lower_gap_division_bridge_ceil + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_division_bridge_ceil. bcs_upper_gap_division_bridge_ceil + S (6 * (e)) = (s * s) + 6)) -> (((2 * (n) = 3 * (q) + (r)) /\ exists bqb_remainder_gap_division_bridge_source. bqb_remainder_gap_division_bridge_source + S (r) = 3)) -> exists c. ((((((q) + (c) = (n)) /\ exists bqb_budget_gap_division_bridge_result. bqb_budget_gap_division_bridge_result + 2 * (n) = 6 * (c))) /\ ((exists bqb_le_gap_division_bridge_ec. bqb_le_gap_division_bridge_ec + (e) = (c)) /\ (exists bqb_le_gap_division_bridge_sum. bqb_le_gap_division_bridge_sum + (q + e) = (n)))) /\ exists bqb_remainder_gap_division_bridge_preserved. bqb_remainder_gap_division_bridge_preserved + S r = 3)

Proof neighborhood

Direct theorem prerequisites

BT00RH canonical_double_triple_remainder_complement_budget BT00RI floor_ceil_complement_budget

Direct theorem dependents

BT00X6 bertrand_main_inequality_factorized_from_total

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

34 script commands · 8 reading checkpoints · 2 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.

Named ingredients (2)
canonical double triple remainder complement budgetfloor ceil complement budget
01Fix variables and assumptionsL1–8

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

  1. L1
    intro n
  2. L2
    intro q
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro e
  6. L6
    intro hfloor
  7. L7
    intro hceil
  8. L8
    intro hcanonical
02Establish hdataL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply canonical double triple remainder complement budget.

  1. L9
    have hdata : ∃ c. q + c = n ∧ Le(2 · n,6 · c) ∧ Lt(r,3)Definitions: Le(2 · n,6 · c)Lt(r,3)Original native command in the exact edition
  2. L10
    specialize canonical_double_triple_remainder_complement_budget n
  3. L11
    specialize canonical_double_triple_remainder_complement_budget q
  4. L12
    specialize canonical_double_triple_remainder_complement_budget r
  5. L13
    apply canonical_double_triple_remainder_complement_budget
  6. L14
    exact hcanonical
03Separate the logical casesL15–17

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

  1. L15
    cases hdata
  2. L16
    cases hdata_witness
  3. L17
    cases hdata_witness_left
04Establish hbridgeL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor ceil complement budget.

  1. L18
    have hbridge : Le(e,x) ∧ Le(q + e,n)Definitions: Le(e,x)Le(q + e,n)Original native command in the exact edition
  2. L19
    specialize floor_ceil_complement_budget n
  3. L20
    specialize floor_ceil_complement_budget q
  4. L21
    specialize floor_ceil_complement_budget s
  5. L22
    specialize floor_ceil_complement_budget e
  6. L23
    specialize floor_ceil_complement_budget x
  7. L24
    apply floor_ceil_complement_budget
  8. L25
    exact hfloor
  9. L26
    exact hceil
  10. L27
    exact hdata_witness_left_left
05Use earlier factsL28–28

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

  1. L28
    exact hdata_witness_left_right
06Construct an explicit witnessL29–29

Supply the displayed value, then prove that it has the required property.

  1. L29
    exists x
07Separate the logical casesL30–31

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

  1. L30
    split
  2. L31
    split
08Use earlier factsL32–34

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

  1. L32
    exact hdata_witness_left
  2. L33
    exact hbridge
  3. L34
    exact hdata_witness_right

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro s
  5. 0005intro e
  6. 0006intro hfloor
  7. 0007intro hceil
  8. 0008intro hcanonical
  9. 0009have hdata : ∃ c. q + c = n ∧ Le(2 · n,6 · c) ∧ Lt(r,3)
    Exact native replay linehave hdata : exists c. (((((q) + (c) = (n)) /\ exists bqb_budget_gap_division_bridge_data. bqb_budget_gap_division_bridge_data + 2 * (n) = 6 * (c))) /\ exists bqb_remainder_gap_division_bridge_data. bqb_remainder_gap_division_bridge_data + S r = 3)
  10. 0010specialize canonical_double_triple_remainder_complement_budget n
  11. 0011specialize canonical_double_triple_remainder_complement_budget q
  12. 0012specialize canonical_double_triple_remainder_complement_budget r
  13. 0013apply canonical_double_triple_remainder_complement_budget
  14. 0014exact hcanonical
  15. 0015cases hdata
  16. 0016cases hdata_witness
  17. 0017cases hdata_witness_left
  18. 0018have hbridge : Le(e,x) ∧ Le(q + e,n)
    Exact native replay linehave hbridge : (exists k. k + e = x) /\ exists k. k + (q + e) = n
  19. 0019specialize floor_ceil_complement_budget n
  20. 0020specialize floor_ceil_complement_budget q
  21. 0021specialize floor_ceil_complement_budget s
  22. 0022specialize floor_ceil_complement_budget e
  23. 0023specialize floor_ceil_complement_budget x
  24. 0024apply floor_ceil_complement_budget
  25. 0025exact hfloor
  26. 0026exact hceil
  27. 0027exact hdata_witness_left_left
  28. 0028exact hdata_witness_left_right
  29. 0029exists x
  30. 0030split
  31. 0031split
  32. 0032exact hdata_witness_left
  33. 0033exact hbridge
  34. 0034exact hdata_witness_right