BT00X1 · Bertrand theorem

six_block_window_decomposition_above_thirty_two

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

Every s>=32 is a six-step iterate of one base root in the exact window 32..37.

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

∀ s. Lt(31,s) → ∃ x. ∃ y. Lt(31,x) ∧ Le(x,37) ∧ s = x + 6 · y

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

3 occurrences

In local proof propositions

PD0001 Le PD0007 DivRem

3 occurrences

Exact expanded native-PA statement
forall s. (exists bqb_le_gap_hjas_decomposition_source. bqb_le_gap_hjas_decomposition_source + (32) = (s)) -> exists b k. (((exists bqb_le_gap_hjas_decomposition_base_lower. bqb_le_gap_hjas_decomposition_base_lower + (32) = (b)) /\ (exists bqb_le_gap_hjas_decomposition_base_upper. bqb_le_gap_hjas_decomposition_base_upper + (b) = (37))) /\ s = b + 6 * k)

Proof neighborhood

Direct theorem prerequisites

BT001P division_remainder_exists BT000C succ_ne_zero BT0017 le_of_succ_le_succ BT0013 le_add_right BT0015 add_le_add_left BT0003 add_assoc BT0002 add_comm

Direct theorem dependents

BT00X3 bertrand_hj_envelope_thirty_two

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

57 script commands · 14 reading checkpoints · 4 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)
division remainder existssucc ne zerole of succ le succle add rightadd le add leftadd assocadd comm
01Fix variables and assumptionsL1–2

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

  1. L1
    intro s
  2. L2
    intro hsource
02Separate the logical casesL3–3

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

  1. L3
    cases hsource
03Establish hdivisionL4–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L4
    have hdivision : ∃ q. ∃ r. DivRem(x,6,q,r)Definitions: DivRem(x,6,q,r)Original native command in the exact edition
  2. L5
    specialize division_remainder_exists 6
  3. L6
    specialize division_remainder_exists x
  4. L7
    apply division_remainder_exists
  5. L8
    intro hzero
  6. L9
    specialize succ_ne_zero 5
  7. L10
    apply succ_ne_zero
  8. L11
    exact hzero
04Separate the logical casesL12–14

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

  1. L12
    cases hdivision
  2. L13
    cases hdivision_witness
  3. L14
    cases hdivision_witness_witness
05Construct an explicit witnessL15–16

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

  1. L15
    exists 32 + x2
  2. L16
    exists x1
06Separate the logical casesL17–18

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

  1. L17
    split
  2. L18
    split
07Use earlier factsL19–21

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

  1. L19
    specialize le_add_right 32
  2. L20
    specialize le_add_right x2
  3. L21
    exact le_add_right
08Establish hremainderL22–26

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

  1. L22
    have hremainder : Le(x2,5)Definitions: Le(x2,5)Original native command in the exact edition
  2. L23
    specialize le_of_succ_le_succ x2
  3. L24
    specialize le_of_succ_le_succ 5
  4. L25
    apply le_of_succ_le_succ
  5. L26
    exact hdivision_witness_witness_right
09Establish hliftedL27–32

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

  1. L27
    have hlifted : Le(32 + x2,32 + 5)Definitions: Le(32 + x2,32 + 5)Original native command in the exact edition
  2. L28
    specialize add_le_add_left x2
  3. L29
    specialize add_le_add_left 5
  4. L30
    specialize add_le_add_left 32
  5. L31
    apply add_le_add_left
  6. L32
    exact hremainder
10Establish hthirty_sevenL33–42

Establish this local claim before using it. It is not an additional assumption.

  1. L33
    have hthirty_seven : 32 + 5 = 37
  2. L34
    norm_num
  3. L35
    rewrite hthirty_seven at hlifted
  4. L36
    exact hlifted
  5. L37
    trans x + 32
  6. L38
    symm
  7. L39
    exact hsource_witness
  8. L40
    trans (6 * x1 + x2) + 32
  9. L41
    congr
  10. L42
    exact hdivision_witness_witness_left
11Calculate and transport equalitiesL43–44

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

  1. L43
    refl
  2. L44
    trans 6 * x1 + (x2 + 32)
12Use earlier factsL45–48

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

  1. L45
    specialize add_assoc (6 * x1)
  2. L46
    specialize add_assoc x2
  3. L47
    specialize add_assoc 32
  4. L48
    apply add_assoc
13Calculate and transport equalitiesL49–51

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

  1. L49
    trans 6 * x1 + (32 + x2)
  2. L50
    congr
  3. L51
    refl
14Use earlier factsL52–57

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

  1. L52
    specialize add_comm x2
  2. L53
    specialize add_comm 32
  3. L54
    apply add_comm
  4. L55
    specialize add_comm (6 * x1)
  5. L56
    specialize add_comm (32 + x2)
  6. L57
    apply add_comm

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro s
  2. 0002intro hsource
  3. 0003cases hsource
  4. 0004have hdivision : ∃ q. ∃ r. DivRem(x,6,q,r)
    Exact native replay linehave hdivision : exists q r. x = 6 * q + r /\ exists h. h + S r = 6
  5. 0005specialize division_remainder_exists 6
  6. 0006specialize division_remainder_exists x
  7. 0007apply division_remainder_exists
  8. 0008intro hzero
  9. 0009specialize succ_ne_zero 5
  10. 0010apply succ_ne_zero
  11. 0011exact hzero
  12. 0012cases hdivision
  13. 0013cases hdivision_witness
  14. 0014cases hdivision_witness_witness
  15. 0015exists 32 + x2
  16. 0016exists x1
  17. 0017split
  18. 0018split
  19. 0019specialize le_add_right 32
  20. 0020specialize le_add_right x2
  21. 0021exact le_add_right
  22. 0022have hremainder : Le(x2,5)
    Exact native replay linehave hremainder : exists bqb_le_gap_hjas_decomposition_remainder_le. bqb_le_gap_hjas_decomposition_remainder_le + (x2) = (5)
  23. 0023specialize le_of_succ_le_succ x2
  24. 0024specialize le_of_succ_le_succ 5
  25. 0025apply le_of_succ_le_succ
  26. 0026exact hdivision_witness_witness_right
  27. 0027have hlifted : Le(32 + x2,32 + 5)
    Exact native replay linehave hlifted : exists bqb_le_gap_hjas_decomposition_lifted_upper. bqb_le_gap_hjas_decomposition_lifted_upper + (32 + x2) = (32 + 5)
  28. 0028specialize add_le_add_left x2
  29. 0029specialize add_le_add_left 5
  30. 0030specialize add_le_add_left 32
  31. 0031apply add_le_add_left
  32. 0032exact hremainder
  33. 0033have hthirty_seven : 32 + 5 = 37
  34. 0034norm_num
  35. 0035rewrite hthirty_seven at hlifted
  36. 0036exact hlifted
  37. 0037trans x + 32
  38. 0038symm
  39. 0039exact hsource_witness
  40. 0040trans (6 * x1 + x2) + 32
  41. 0041congr
  42. 0042exact hdivision_witness_witness_left
  43. 0043refl
  44. 0044trans 6 * x1 + (x2 + 32)
  45. 0045specialize add_assoc (6 * x1)
  46. 0046specialize add_assoc x2
  47. 0047specialize add_assoc 32
  48. 0048apply add_assoc
  49. 0049trans 6 * x1 + (32 + x2)
  50. 0050congr
  51. 0051refl
  52. 0052specialize add_comm x2
  53. 0053specialize add_comm 32
  54. 0054apply add_comm
  55. 0055specialize add_comm (6 * x1)
  56. 0056specialize add_comm (32 + x2)
  57. 0057apply add_comm