BT00RA · Bertrand theorem

floor_sqrt_total

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

Every natural lies in a constructively selected adjacent-square interval.

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

∀ x. ∃ s. FloorSqrt(x,s)

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

PD0051 FloorSqrt

1 occurrences

In local proof propositions

PD0002 Lt

1 occurrences

Exact expanded native-PA statement
forall x. exists s. (((exists bcs_sqrt_lower_gap_total_result. bcs_sqrt_lower_gap_total_result + (s) * (s) = (x)) /\ exists bcs_sqrt_upper_gap_total_result. bcs_sqrt_upper_gap_total_result + S (x) = S (s) * S (s)))

Proof neighborhood

Direct theorem prerequisites

BT00R9 square_lt_successor_square BT001C le_eq_or_lt BT0000 zero_add BT0018 le_succ

Direct theorem dependents

BT0115 bertrand_eventually_closed_upper

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

32 script commands · 22 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 (4)
square lt successor squarele eq or ltzero addle succ
01Induction on xL1–1

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction x
02Construct an explicit witnessL2–2

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

  1. L2
    exists 0
03Separate the logical casesL3–3

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

  1. L3
    split
04Construct an explicit witnessL4–4

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

  1. L4
    exists 0
05Calculate and transport equalitiesL5–5

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

  1. L5
    norm_num
06Construct an explicit witnessL6–6

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

  1. L6
    exists 0
07Calculate and transport equalitiesL7–7

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

  1. L7
    norm_num
08Separate the logical casesL8–9

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

  1. L8
    cases IH
  2. L9
    cases IH_witness
09Establish hsplitL10–14

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

  1. L10
    have hsplit : S x = S x1 · S x1 ∨ Lt(S x,S x1 · S x1)Definitions: Lt(S x,S x1 · S x1)Original native command in the exact edition
  2. L11
    specialize le_eq_or_lt (S x)
  3. L12
    specialize le_eq_or_lt (S x1 * S x1)
  4. L13
    apply le_eq_or_lt
  5. L14
    exact IH_witness_right
10Separate the logical casesL15–15

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

  1. L15
    cases hsplit
11Construct an explicit witnessL16–16

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

  1. L16
    exists S x1
12Separate the logical casesL17–17

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

  1. L17
    split
13Construct an explicit witnessL18–18

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

  1. L18
    exists 0
14Calculate and transport equalitiesL19–19

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

  1. L19
    trans S x1 * S x1
15Use earlier factsL20–20

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

  1. L20
    apply zero_add
16Calculate and transport equalitiesL21–21

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

  1. L21
    symm
17Use earlier factsL22–23

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

  1. L22
    exact hsplit_left
  2. L23
    specialize square_lt_successor_square (S x1)
18Calculate and transport equalitiesL24–24

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

  1. L24
    rewrite hsplit_left
19Use earlier factsL25–25

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

  1. L25
    exact square_lt_successor_square
20Construct an explicit witnessL26–26

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

  1. L26
    exists x1
21Separate the logical casesL27–27

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

  1. L27
    split
22Use earlier factsL28–32

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

  1. L28
    specialize le_succ (x1 * x1)
  2. L29
    specialize le_succ x
  3. L30
    apply le_succ
  4. L31
    exact IH_witness_left
  5. L32
    exact hsplit_right

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001induction x
  2. 0002exists 0
  3. 0003split
  4. 0004exists 0
  5. 0005norm_num
  6. 0006exists 0
  7. 0007norm_num
  8. 0008cases IH
  9. 0009cases IH_witness
  10. 0010have hsplit : S x = S x1 · S x1 ∨ Lt(S x,S x1 · S x1)
    Exact native replay linehave hsplit : S x = S x1 * S x1 \/ exists k. k + S (S x) = S x1 * S x1
  11. 0011specialize le_eq_or_lt (S x)
  12. 0012specialize le_eq_or_lt (S x1 * S x1)
  13. 0013apply le_eq_or_lt
  14. 0014exact IH_witness_right
  15. 0015cases hsplit
  16. 0016exists S x1
  17. 0017split
  18. 0018exists 0
  19. 0019trans S x1 * S x1
  20. 0020apply zero_add
  21. 0021symm
  22. 0022exact hsplit_left
  23. 0023specialize square_lt_successor_square (S x1)
  24. 0024rewrite hsplit_left
  25. 0025exact square_lt_successor_square
  26. 0026exists x1
  27. 0027split
  28. 0028specialize le_succ (x1 * x1)
  29. 0029specialize le_succ x
  30. 0030apply le_succ
  31. 0031exact IH_witness_left
  32. 0032exact hsplit_right