BT00RI · Bertrand theorem

floor_ceil_complement_budget

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

Floor-square and ceiling budgets imply e<=c and q+e<=n.

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. ∀ s. ∀ e. ∀ c. FloorSqrt(2 · n,s) → CeilDivSix(s · s,e) → q + c = n → Le(2 · n,6 · c) → Le(e,c) ∧ Le(q + e,n)

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 PD0051 FloorSqrt PD0052 CeilDivSix

5 occurrences

In local proof propositions

PD0001 Le

3 occurrences

Exact expanded native-PA statement
forall n q s e c. (((exists bcs_sqrt_lower_gap_complement_bridge_floor. bcs_sqrt_lower_gap_complement_bridge_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_complement_bridge_floor. bcs_sqrt_upper_gap_complement_bridge_floor + S (2 * n) = S (s) * S (s))) -> (((exists bcs_lower_gap_complement_bridge_ceil. bcs_lower_gap_complement_bridge_ceil + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_complement_bridge_ceil. bcs_upper_gap_complement_bridge_ceil + S (6 * (e)) = (s * s) + 6)) -> q + c = n -> (exists k. k + 2 * n = 6 * c) -> ((exists bqb_le_gap_complement_bridge_ec. bqb_le_gap_complement_bridge_ec + (e) = (c)) /\ (exists bqb_le_gap_complement_bridge_sum. bqb_le_gap_complement_bridge_sum + (q + e) = (n)))

Proof neighborhood

Direct theorem prerequisites

BT000F le_trans BT00RF ceil_div_six_le_of_upper BT0015 add_le_add_left

Direct theorem dependents

BT00RJ floor_ceil_division_budget

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 · 9 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.

Named ingredients (3)
le transceil div six le of upperadd le add left
01Fix variables and assumptionsL1–9

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

  1. L1
    intro n
  2. L2
    intro q
  3. L3
    intro s
  4. L4
    intro e
  5. L5
    intro c
  6. L6
    intro hfloor
  7. L7
    intro hceil
  8. L8
    intro hcomp
  9. L9
    intro hbudget
02Separate the logical casesL10–10

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

  1. L10
    cases hfloor
03Establish hsquareL11–17

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

  1. L11
    have hsquare : Le(s · s,6 · c)Definitions: Le(s · s,6 · c)Original native command in the exact edition
  2. L12
    specialize le_trans (s * s)
  3. L13
    specialize le_trans (2 * n)
  4. L14
    specialize le_trans (6 * c)
  5. L15
    apply le_trans
  6. L16
    exact hfloor_left
  7. L17
    exact hbudget
04Establish hecL18–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ceil div six le of upper.

  1. L18
  2. L19
    specialize ceil_div_six_le_of_upper (s * s)
  3. L20
    specialize ceil_div_six_le_of_upper e
  4. L21
    specialize ceil_div_six_le_of_upper c
  5. L22
    apply ceil_div_six_le_of_upper
  6. L23
    exact hceil
  7. L24
    exact hsquare
05Establish hsumL25–30

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

  1. L25
    have hsum : Le(q + e,q + c)Definitions: Le(q + e,q + c)Original native command in the exact edition
  2. L26
    specialize add_le_add_left e
  3. L27
    specialize add_le_add_left c
  4. L28
    specialize add_le_add_left q
  5. L29
    apply add_le_add_left
  6. L30
    exact hec
06Separate the logical casesL31–31

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

  1. L31
    split
07Use earlier factsL32–32

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

  1. L32
    exact hec
08Calculate and transport equalitiesL33–33

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

  1. L33
    rewrite <- hcomp
09Use earlier factsL34–34

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

  1. L34
    exact hsum

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro n
  2. 0002intro q
  3. 0003intro s
  4. 0004intro e
  5. 0005intro c
  6. 0006intro hfloor
  7. 0007intro hceil
  8. 0008intro hcomp
  9. 0009intro hbudget
  10. 0010cases hfloor
  11. 0011have hsquare : Le(s · s,6 · c)
    Exact native replay linehave hsquare : exists k. k + s * s = 6 * c
  12. 0012specialize le_trans (s * s)
  13. 0013specialize le_trans (2 * n)
  14. 0014specialize le_trans (6 * c)
  15. 0015apply le_trans
  16. 0016exact hfloor_left
  17. 0017exact hbudget
  18. 0018have hec : Le(e,c)
    Exact native replay linehave hec : exists k. k + e = c
  19. 0019specialize ceil_div_six_le_of_upper (s * s)
  20. 0020specialize ceil_div_six_le_of_upper e
  21. 0021specialize ceil_div_six_le_of_upper c
  22. 0022apply ceil_div_six_le_of_upper
  23. 0023exact hceil
  24. 0024exact hsquare
  25. 0025have hsum : Le(q + e,q + c)
    Exact native replay linehave hsum : exists k. k + (q + e) = q + c
  26. 0026specialize add_le_add_left e
  27. 0027specialize add_le_add_left c
  28. 0028specialize add_le_add_left q
  29. 0029apply add_le_add_left
  30. 0030exact hec
  31. 0031split
  32. 0032exact hec
  33. 0033rewrite <- hcomp
  34. 0034exact hsum