BT00PS · Bertrand theorem

bounded_prime_interval_search

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

Bounded search returns a prime witness or an explicit prime-free interval certificate.

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

∀ l. ∀ u. (∃ x. Prime(x) ∧ (Lt(l,x) ∧ Le(x,u))) ∨ (∀ x. Lt(l,x) ∧ Le(x,u) → ¬Prime(x))

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 PD0004 Prime

6 occurrences

In local proof propositions

PD0002 Lt

1 occurrences

Exact expanded native-PA statement
forall l u. (exists bpi_value_search_witness. ((((~(bpi_value_search_witness = 1) /\ forall frm_prime_left_bpi_search_witness_interval_prime frm_prime_right_bpi_search_witness_interval_prime. bpi_value_search_witness = frm_prime_left_bpi_search_witness_interval_prime * frm_prime_right_bpi_search_witness_interval_prime -> frm_prime_left_bpi_search_witness_interval_prime = 1 \/ frm_prime_right_bpi_search_witness_interval_prime = 1)) /\ ((exists frm_gap_bpi_search_witness_interval_lower. frm_gap_bpi_search_witness_interval_lower + S l = bpi_value_search_witness) /\ (exists frm_weak_gap_bpi_search_witness_interval_upper. frm_weak_gap_bpi_search_witness_interval_upper + bpi_value_search_witness = u))))) \/ (forall bpi_value_search_exclusion. ((exists frm_gap_bpi_search_exclusion_lower. frm_gap_bpi_search_exclusion_lower + S l = bpi_value_search_exclusion) /\ (exists frm_weak_gap_bpi_search_exclusion_upper. frm_weak_gap_bpi_search_exclusion_upper + bpi_value_search_exclusion = u)) -> ~((~(bpi_value_search_exclusion = 1) /\ forall frm_prime_left_bpi_search_exclusion_prime frm_prime_right_bpi_search_exclusion_prime. bpi_value_search_exclusion = frm_prime_left_bpi_search_exclusion_prime * frm_prime_right_bpi_search_exclusion_prime -> frm_prime_left_bpi_search_exclusion_prime = 1 \/ frm_prime_right_bpi_search_exclusion_prime = 1)))

Proof neighborhood

Direct theorem prerequisites

BT003G prime_nonzero BT000Y le_zero BT00PR prime_strictly_above_decidable BT000E le_refl BT0018 le_succ BT001C le_eq_or_lt BT0017 le_of_succ_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

68 script commands · 35 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 (7)
prime nonzerole zeroprime strictly above decidablele reflle succle eq or ltle of succ le succ
01Fix variables and assumptionsL1–1

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

  1. L1
    intro l
02Induction on uL2–2

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

  1. L2
    induction u
03Separate the logical casesL3–3

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

  1. L3
    right
04Fix variables and assumptionsL4–5

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

  1. L4
    intro p
  2. L5
    intro hbounds
05Separate the logical casesL6–6

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

  1. L6
    cases hbounds
06Fix variables and assumptionsL7–7

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

  1. L7
    intro hp
07Use earlier factsL8–8

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

  1. L8
    specialize le_zero p
08Establish hzeroL9–17

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

  1. L9
    have hzero : p = 0
  2. L10
    apply le_zero
  3. L11
    exact hbounds_right
  4. L12
    specialize prime_nonzero p
  5. L13
    apply prime_nonzero
  6. L14
    exact hp
  7. L15
    exact hzero
  8. L16
    specialize prime_strictly_above_decidable l
  9. L17
    specialize prime_strictly_above_decidable (S u)
09Separate the logical casesL18–19

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

  1. L18
    cases prime_strictly_above_decidable
  2. L19
    left
10Construct an explicit witnessL20–20

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

  1. L20
    exists S u
11Separate the logical casesL21–22

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

  1. L21
    cases prime_strictly_above_decidable_left
  2. L22
    split
12Use earlier factsL23–23

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

  1. L23
    exact prime_strictly_above_decidable_left_left
13Separate the logical casesL24–24

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

  1. L24
    split
14Use earlier factsL25–27

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

  1. L25
    exact prime_strictly_above_decidable_left_right
  2. L26
    specialize le_refl (S u)
  3. L27
    exact le_refl
15Separate the logical casesL28–30

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

  1. L28
    cases IH
  2. L29
    left
  3. L30
    cases IH_left
16Construct an explicit witnessL31–31

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

  1. L31
    exists x
17Separate the logical casesL32–34

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

  1. L32
    cases IH_left_witness
  2. L33
    cases IH_left_witness_right
  3. L34
    split
18Use earlier factsL35–35

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

  1. L35
    exact IH_left_witness_left
19Separate the logical casesL36–36

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

  1. L36
    split
20Use earlier factsL37–41

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

  1. L37
    exact IH_left_witness_right_left
  2. L38
    specialize le_succ x
  3. L39
    specialize le_succ u
  4. L40
    apply le_succ
  5. L41
    exact IH_left_witness_right_right
21Separate the logical casesL42–42

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

  1. L42
    right
22Fix variables and assumptionsL43–44

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

  1. L43
    intro p
  2. L44
    intro hbounds
23Separate the logical casesL45–45

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

  1. L45
    cases hbounds
24Fix variables and assumptionsL46–46

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

  1. L46
    intro hp
25Use earlier factsL47–48

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

  1. L47
    specialize le_eq_or_lt p
  2. L48
    specialize le_eq_or_lt (S u)
26Establish hsplitL49–51

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

  1. L49
    have hsplit : p = S u ∨ Lt(p,S u)Definitions: Lt(p,S u)Original native command in the exact edition
  2. L50
    apply le_eq_or_lt
  3. L51
    exact hbounds_right
27Separate the logical casesL52–52

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

  1. L52
    cases hsplit
28Use earlier factsL53–53

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

  1. L53
    apply prime_strictly_above_decidable_right
29Separate the logical casesL54–54

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

  1. L54
    split
30Calculate and transport equalitiesL55–56

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

  1. L55
    rewrite hsplit_left at hp
  2. L56
    rewrite hsplit_left at hp
31Use earlier factsL57–57

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

  1. L57
    exact hp
32Calculate and transport equalitiesL58–58

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

  1. L58
    rewrite hsplit_left at hbounds_left
33Use earlier factsL59–61

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

  1. L59
    exact hbounds_left
  2. L60
    specialize IH_right p
  3. L61
    apply IH_right
34Separate the logical casesL62–62

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

  1. L62
    split
35Use earlier factsL63–68

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

  1. L63
    exact hbounds_left
  2. L64
    specialize le_of_succ_le_succ p
  3. L65
    specialize le_of_succ_le_succ u
  4. L66
    apply le_of_succ_le_succ
  5. L67
    exact hsplit_right
  6. L68
    exact hp

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro l
  2. 0002induction u
  3. 0003right
  4. 0004intro p
  5. 0005intro hbounds
  6. 0006cases hbounds
  7. 0007intro hp
  8. 0008specialize le_zero p
  9. 0009have hzero : p = 0
  10. 0010apply le_zero
  11. 0011exact hbounds_right
  12. 0012specialize prime_nonzero p
  13. 0013apply prime_nonzero
  14. 0014exact hp
  15. 0015exact hzero
  16. 0016specialize prime_strictly_above_decidable l
  17. 0017specialize prime_strictly_above_decidable (S u)
  18. 0018cases prime_strictly_above_decidable
  19. 0019left
  20. 0020exists S u
  21. 0021cases prime_strictly_above_decidable_left
  22. 0022split
  23. 0023exact prime_strictly_above_decidable_left_left
  24. 0024split
  25. 0025exact prime_strictly_above_decidable_left_right
  26. 0026specialize le_refl (S u)
  27. 0027exact le_refl
  28. 0028cases IH
  29. 0029left
  30. 0030cases IH_left
  31. 0031exists x
  32. 0032cases IH_left_witness
  33. 0033cases IH_left_witness_right
  34. 0034split
  35. 0035exact IH_left_witness_left
  36. 0036split
  37. 0037exact IH_left_witness_right_left
  38. 0038specialize le_succ x
  39. 0039specialize le_succ u
  40. 0040apply le_succ
  41. 0041exact IH_left_witness_right_right
  42. 0042right
  43. 0043intro p
  44. 0044intro hbounds
  45. 0045cases hbounds
  46. 0046intro hp
  47. 0047specialize le_eq_or_lt p
  48. 0048specialize le_eq_or_lt (S u)
  49. 0049have hsplit : p = S u ∨ Lt(p,S u)
    Exact native replay linehave hsplit : p = S u \/ exists h. h + S p = S u
  50. 0050apply le_eq_or_lt
  51. 0051exact hbounds_right
  52. 0052cases hsplit
  53. 0053apply prime_strictly_above_decidable_right
  54. 0054split
  55. 0055rewrite hsplit_left at hp
  56. 0056rewrite hsplit_left at hp
  57. 0057exact hp
  58. 0058rewrite hsplit_left at hbounds_left
  59. 0059exact hbounds_left
  60. 0060specialize IH_right p
  61. 0061apply IH_right
  62. 0062split
  63. 0063exact hbounds_left
  64. 0064specialize le_of_succ_le_succ p
  65. 0065specialize le_of_succ_le_succ u
  66. 0066apply le_of_succ_le_succ
  67. 0067exact hsplit_right
  68. 0068exact hp