BT010D

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.

Exact expanded 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)

Structural proof guide

Three times the floor root lies below the doubled input.

Direct prerequisites: two_lt_double_lower_six, floor_sqrt_two_le_of_two_lt, three_mul_le_square_of_three_le, le_eq_or_lt, floor_sqrt_lower_bound, le_trans. The authored body proceeds by case analysis (1), intermediate claims (7), equality transport (2), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

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 dependents

BT010F floor_sqrt_le_third_quotient

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

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.

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
    have htwo : exists bcf_le_gap_b5rbfstmd_two. bcf_le_gap_b5rbfstmd_two + (2) = s
  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 \/ (exists bcf_lt_gap_b5rbfstmd_strict. bcf_lt_gap_b5rbfstmd_strict + S (2) = s)
  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 : exists bcf_le_gap_b5rbfstmd_lower_six. bcf_le_gap_b5rbfstmd_lower_six + (3 + 3) = n + n
  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 : exists bcf_le_gap_b5rbfstmd_three. bcf_le_gap_b5rbfstmd_three + (3) = s
  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 : exists bcf_le_gap_b5rbfstmd_square. bcf_le_gap_b5rbfstmd_square + (3 * s) = s * s
  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 : exists bcf_le_gap_b5rbfstmd_floor_lower. bcf_le_gap_b5rbfstmd_floor_lower + (s * s) = n + n
  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 exact command ledger · 42 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro hpositive
  4. 0004intro hfloor
  5. 0005have 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 \/ (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 : 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 : exists bcf_le_gap_b5rbfstmd_three. bcf_le_gap_b5rbfstmd_three + (3) = s
  27. 0027exact hsplit_right
  28. 0028have 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 : 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