BT010J · Bertrand theorem

floor_third_double_gap_package

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

Package the two exact additive gaps used by the three-range split.

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) → ∃ x. ∃ y. s + x = q ∧ q + y = 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

PD0002 Lt PD0007 DivRem PD0051 FloorSqrt

3 occurrences

In local proof propositions

none

0 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 g h. s + g = q /\ q + h = n + n

Proof neighborhood

Direct theorem prerequisites

BT010G floor_sqrt_third_quotient_gap_exists BT010I third_quotient_double_gap_exists

Direct theorem dependents

BT0114 central_binom_le_of_no_bertrand_prime

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

29 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)
floor sqrt third quotient gap existsthird quotient double gap exists
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 hfirstL8–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor sqrt third quotient gap exists.

  1. L8
    have hfirst : exists g. s + g = q
  2. L9
    specialize floor_sqrt_third_quotient_gap_exists n
  3. L10
    specialize floor_sqrt_third_quotient_gap_exists s
  4. L11
    specialize floor_sqrt_third_quotient_gap_exists q
  5. L12
    specialize floor_sqrt_third_quotient_gap_exists r
  6. L13
    apply floor_sqrt_third_quotient_gap_exists
  7. L14
    exact hpositive
  8. L15
    exact hfloor
  9. L16
    exact hdivision
03Separate the logical casesL17–17

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

  1. L17
    cases hfirst
04Establish hsecondL18–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply third quotient double gap exists.

  1. L18
    have hsecond : exists h. q + h = n + n
  2. L19
    specialize third_quotient_double_gap_exists n
  3. L20
    specialize third_quotient_double_gap_exists q
  4. L21
    specialize third_quotient_double_gap_exists r
  5. L22
    apply third_quotient_double_gap_exists
  6. L23
    exact hdivision
05Separate the logical casesL24–24

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

  1. L24
    cases hsecond
06Construct an explicit witnessL25–26

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

  1. L25
    exists x
  2. L26
    exists x1
07Separate the logical casesL27–27

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

  1. L27
    split
08Use earlier factsL28–29

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

  1. L28
    exact hfirst_witness
  2. L29
    exact hsecond_witness

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hpositive
  6. 0006intro hfloor
  7. 0007intro hdivision
  8. 0008have hfirst : exists g. s + g = q
  9. 0009specialize floor_sqrt_third_quotient_gap_exists n
  10. 0010specialize floor_sqrt_third_quotient_gap_exists s
  11. 0011specialize floor_sqrt_third_quotient_gap_exists q
  12. 0012specialize floor_sqrt_third_quotient_gap_exists r
  13. 0013apply floor_sqrt_third_quotient_gap_exists
  14. 0014exact hpositive
  15. 0015exact hfloor
  16. 0016exact hdivision
  17. 0017cases hfirst
  18. 0018have hsecond : exists h. q + h = n + n
  19. 0019specialize third_quotient_double_gap_exists n
  20. 0020specialize third_quotient_double_gap_exists q
  21. 0021specialize third_quotient_double_gap_exists r
  22. 0022apply third_quotient_double_gap_exists
  23. 0023exact hdivision
  24. 0024cases hsecond
  25. 0025exists x
  26. 0026exists x1
  27. 0027split
  28. 0028exact hfirst_witness
  29. 0029exact hsecond_witness