BT010D · Bertrand theorem

floor_sqrt_three_mul_le_double

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

Three times the floor root lies below the doubled input.

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. ∀ s. Lt(2,n) → FloorSqrt(n + n,s) → Le(3 · s,n + 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 PD0002 Lt PD0051 FloorSqrt

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

6 occurrences

Exact expanded native-PA statement
forall n s. (exists bcf_lt_gap_b5rbfstmd_positive. bcf_lt_gap_b5rbfstmd_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5rbfstmd_floor. bcs_sqrt_lower_gap_b5rbfstmd_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5rbfstmd_floor. bcs_sqrt_upper_gap_b5rbfstmd_floor + S (n + n) = S (s) * S (s))) -> (exists bcf_le_gap_b5rbfstmd_result. bcf_le_gap_b5rbfstmd_result + (3 * s) = n + n)

Proof neighborhood

Direct theorem prerequisites

BT010A two_lt_double_lower_six BT010B floor_sqrt_two_le_of_two_lt BT010C three_mul_le_square_of_three_le BT001C le_eq_or_lt BT00R6 floor_sqrt_lower_bound BT000F le_trans

Direct theorem dependents

BT010F floor_sqrt_le_third_quotient

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

42 script commands · 10 reading checkpoints · 7 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 (6)
two lt double lower sixfloor sqrt two le of two ltthree mul le square of three lele eq or ltfloor sqrt lower boundle trans
01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro s
  3. L3
    intro hpositive
  4. L4
    intro hfloor
02Establish htwoL5–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor sqrt two le of two lt.

  1. L5
  2. L6
    specialize floor_sqrt_two_le_of_two_lt n
  3. L7
    specialize floor_sqrt_two_le_of_two_lt s
  4. L8
    apply floor_sqrt_two_le_of_two_lt
  5. L9
    exact hpositive
  6. L10
    exact hfloor
03Establish hsplitL11–15

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

  1. L11
    have hsplit : 2 = s ∨ Lt(2,s)Definitions: Lt(2,s)Original native command in the exact edition
  2. L12
    specialize le_eq_or_lt 2
  3. L13
    specialize le_eq_or_lt s
  4. L14
    apply le_eq_or_lt
  5. L15
    exact htwo
04Separate the logical casesL16–16

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

  1. L16
    cases hsplit
05Establish hlowerL17–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply two lt double lower six.

  1. L17
    have hlower : Le(3 + 3,n + n)Definitions: Le(3 + 3,n + n)Original native command in the exact edition
  2. L18
    specialize two_lt_double_lower_six n
  3. L19
    apply two_lt_double_lower_six
  4. L20
    exact hpositive
  5. L21
    rewrite <- hsplit_left
06Establish hcalcL22–25

Establish this local claim before using it. It is not an additional assumption.

  1. L22
    have hcalc : 3 * 2 = 3 + 3
  2. L23
    norm_num
  3. L24
    rewrite hcalc
  4. L25
    exact hlower
07Establish hthreeL26–27

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hthree : Lt(2,s)Definitions: Lt(2,s)Original native command in the exact edition
  2. L27
    exact hsplit_right
08Establish hsquareL28–31

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

  1. L28
    have hsquare : Le(3 · s,s · s)Definitions: Le(3 · s,s · s)Original native command in the exact edition
  2. L29
    specialize three_mul_le_square_of_three_le s
  3. L30
    apply three_mul_le_square_of_three_le
  4. L31
    exact hthree
09Establish hfloor_lowerL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor sqrt lower bound.

  1. L32
    have hfloor_lower : Le(s · s,n + n)Definitions: Le(s · s,n + n)Original native command in the exact edition
  2. L33
    specialize floor_sqrt_lower_bound (n + n)
  3. L34
    specialize floor_sqrt_lower_bound s
  4. L35
    apply floor_sqrt_lower_bound
  5. L36
    exact hfloor
  6. L37
    specialize le_trans (3 * s)
  7. L38
    specialize le_trans (s * s)
  8. L39
    specialize le_trans (n + n)
  9. L40
    apply le_trans
  10. L41
    exact hsquare
10Use earlier factsL42–42

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

  1. L42
    exact hfloor_lower

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro hpositive
  4. 0004intro hfloor
  5. 0005have htwo : Lt(1,s)
    Exact native replay linehave htwo : exists bcf_le_gap_b5rbfstmd_two. bcf_le_gap_b5rbfstmd_two + (2) = s
  6. 0006specialize floor_sqrt_two_le_of_two_lt n
  7. 0007specialize floor_sqrt_two_le_of_two_lt s
  8. 0008apply floor_sqrt_two_le_of_two_lt
  9. 0009exact hpositive
  10. 0010exact hfloor
  11. 0011have hsplit : 2 = s ∨ Lt(2,s)
    Exact native replay linehave hsplit : 2 = s \/ (exists bcf_lt_gap_b5rbfstmd_strict. bcf_lt_gap_b5rbfstmd_strict + S (2) = s)
  12. 0012specialize le_eq_or_lt 2
  13. 0013specialize le_eq_or_lt s
  14. 0014apply le_eq_or_lt
  15. 0015exact htwo
  16. 0016cases hsplit
  17. 0017have hlower : Le(3 + 3,n + n)
    Exact native replay linehave hlower : exists bcf_le_gap_b5rbfstmd_lower_six. bcf_le_gap_b5rbfstmd_lower_six + (3 + 3) = n + n
  18. 0018specialize two_lt_double_lower_six n
  19. 0019apply two_lt_double_lower_six
  20. 0020exact hpositive
  21. 0021rewrite <- hsplit_left
  22. 0022have hcalc : 3 * 2 = 3 + 3
  23. 0023norm_num
  24. 0024rewrite hcalc
  25. 0025exact hlower
  26. 0026have hthree : Lt(2,s)
    Exact native replay linehave hthree : exists bcf_le_gap_b5rbfstmd_three. bcf_le_gap_b5rbfstmd_three + (3) = s
  27. 0027exact hsplit_right
  28. 0028have hsquare : Le(3 · s,s · s)
    Exact native replay linehave hsquare : exists bcf_le_gap_b5rbfstmd_square. bcf_le_gap_b5rbfstmd_square + (3 * s) = s * s
  29. 0029specialize three_mul_le_square_of_three_le s
  30. 0030apply three_mul_le_square_of_three_le
  31. 0031exact hthree
  32. 0032have hfloor_lower : Le(s · s,n + n)
    Exact native replay linehave hfloor_lower : exists bcf_le_gap_b5rbfstmd_floor_lower. bcf_le_gap_b5rbfstmd_floor_lower + (s * s) = n + n
  33. 0033specialize floor_sqrt_lower_bound (n + n)
  34. 0034specialize floor_sqrt_lower_bound s
  35. 0035apply floor_sqrt_lower_bound
  36. 0036exact hfloor
  37. 0037specialize le_trans (3 * s)
  38. 0038specialize le_trans (s * s)
  39. 0039specialize le_trans (n + n)
  40. 0040apply le_trans
  41. 0041exact hsquare
  42. 0042exact hfloor_lower