BT010F · Bertrand theorem

floor_sqrt_le_third_quotient

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

The floor root is at most the quotient of the doubled input by three.

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. ∀ q. ∀ r. Lt(2,n) → FloorSqrt(n + n,s) → DivRem(n + n,3,q,r) → Le(s,q)

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

4 occurrences

In local proof propositions

PD0001 Le

1 occurrences

Exact expanded native-PA statement
forall n s q r. (exists bcf_lt_gap_b5rbfsltq_positive. bcf_lt_gap_b5rbfsltq_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5rbfsltq_floor. bcs_sqrt_lower_gap_b5rbfsltq_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5rbfsltq_floor. bcs_sqrt_upper_gap_b5rbfsltq_floor + S (n + n) = S (s) * S (s))) -> (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_b5rbfsltq_division_bound. bcf_lt_gap_b5rbfsltq_division_bound + S (r) = 3))) -> (exists bcf_le_gap_b5rbfsltq_result. bcf_le_gap_b5rbfsltq_result + (s) = q)

Proof neighborhood

Direct theorem prerequisites

BT010D floor_sqrt_three_mul_le_double BT010E division_quotient_lower_of_scaled_le

Direct theorem dependents

BT010G floor_sqrt_third_quotient_gap_exists BT010X no_bertrand_high_contribution_choice_eq_one

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

21 script commands · 3 reading checkpoints · 1 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)
floor sqrt three mul le doubledivision quotient lower of scaled le
01Fix variables and assumptionsL1–7

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

  1. L1
    intro n
  2. L2
    intro s
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro hpositive
  6. L6
    intro hfloor
  7. L7
    intro hdivision
02Establish hscaledL8–17

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

  1. L8
    have hscaled : Le(3 · s,n + n)Definitions: Le(3 · s,n + n)Original native command in the exact edition
  2. L9
    specialize floor_sqrt_three_mul_le_double n
  3. L10
    specialize floor_sqrt_three_mul_le_double s
  4. L11
    apply floor_sqrt_three_mul_le_double
  5. L12
    exact hpositive
  6. L13
    exact hfloor
  7. L14
    specialize division_quotient_lower_of_scaled_le 3
  8. L15
    specialize division_quotient_lower_of_scaled_le (n + n)
  9. L16
    specialize division_quotient_lower_of_scaled_le q
  10. L17
    specialize division_quotient_lower_of_scaled_le r
03Use earlier factsL18–21

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

  1. L18
    specialize division_quotient_lower_of_scaled_le s
  2. L19
    apply division_quotient_lower_of_scaled_le
  3. L20
    exact hdivision
  4. L21
    exact hscaled

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hpositive
  6. 0006intro hfloor
  7. 0007intro hdivision
  8. 0008have hscaled : Le(3 · s,n + n)
    Exact native replay linehave hscaled : exists bcf_le_gap_b5rbfsltq_scaled. bcf_le_gap_b5rbfsltq_scaled + (3 * s) = n + n
  9. 0009specialize floor_sqrt_three_mul_le_double n
  10. 0010specialize floor_sqrt_three_mul_le_double s
  11. 0011apply floor_sqrt_three_mul_le_double
  12. 0012exact hpositive
  13. 0013exact hfloor
  14. 0014specialize division_quotient_lower_of_scaled_le 3
  15. 0015specialize division_quotient_lower_of_scaled_le (n + n)
  16. 0016specialize division_quotient_lower_of_scaled_le q
  17. 0017specialize division_quotient_lower_of_scaled_le r
  18. 0018specialize division_quotient_lower_of_scaled_le s
  19. 0019apply division_quotient_lower_of_scaled_le
  20. 0020exact hdivision
  21. 0021exact hscaled