BT011Q

bertrand_covering_interval

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

One checked adjacent cover supplies a Bertrand witness.

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.

Exact expanded PA statement

forall a b n. ((~(b = 1) /\ forall bpr_left_bb8ci_prime bpr_right_bb8ci_prime. b = bpr_left_bb8ci_prime * bpr_right_bb8ci_prime -> bpr_left_bb8ci_prime = 1 \/ bpr_right_bb8ci_prime = 1)) -> (exists bpr_le_gap_bb8ci_lower. bpr_le_gap_bb8ci_lower + (a) = (n)) -> (exists bpr_gap_bb8ci_strict. bpr_gap_bb8ci_strict + S (n) = b) -> (exists bpr_le_gap_bb8ci_cover. bpr_le_gap_bb8ci_cover + (b) = (a + a)) -> exists p. ((~(p = 1) /\ forall bpr_left_bb8ci_result_prime bpr_right_bb8ci_result_prime. p = bpr_left_bb8ci_result_prime * bpr_right_bb8ci_result_prime -> bpr_left_bb8ci_result_prime = 1 \/ bpr_right_bb8ci_result_prime = 1)) /\ ((exists bpr_gap_bb8ci_result_strict. bpr_gap_bb8ci_result_strict + S (n) = p) /\ (exists bpr_le_gap_bb8ci_result_upper. bpr_le_gap_bb8ci_result_upper + (p) = (n + n)))

Structural proof guide

One checked adjacent cover supplies a Bertrand witness.

Direct prerequisites: add_le_add_right, add_le_add_left, le_trans. The authored body proceeds by intermediate claims (4).

Proof neighborhood

Direct dependencies

BT0014 add_le_add_right BT0015 add_le_add_left BT000F le_trans

Direct dependents

BT0124 bertrand_small_closed_upper

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

39 script commands · 10 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.

Named ingredients (3)
add le add rightadd le add leftle trans
01Fix variables and assumptionsL1–7

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro n
  4. L4
    intro hprime
  5. L5
    intro hlower
  6. L6
    intro hstrict
  7. L7
    intro hcover
02Establish hfirstL8–13

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

  1. L8
    have hfirst : exists k. k + (a + a) = n + a
  2. L9
    specialize add_le_add_right a
  3. L10
    specialize add_le_add_right n
  4. L11
    specialize add_le_add_right a
  5. L12
    apply add_le_add_right
  6. L13
    exact hlower
03Establish hsecondL14–19

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

  1. L14
    have hsecond : exists k. k + (n + a) = n + n
  2. L15
    specialize add_le_add_left a
  3. L16
    specialize add_le_add_left n
  4. L17
    specialize add_le_add_left n
  5. L18
    apply add_le_add_left
  6. L19
    exact hlower
04Establish hdoubleL20–26

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

  1. L20
    have hdouble : exists k. k + (a + a) = n + n
  2. L21
    specialize le_trans (a + a)
  3. L22
    specialize le_trans (n + a)
  4. L23
    specialize le_trans (n + n)
  5. L24
    apply le_trans
  6. L25
    exact hfirst
  7. L26
    exact hsecond
05Establish hupperL27–33

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

  1. L27
    have hupper : exists k. k + b = n + n
  2. L28
    specialize le_trans b
  3. L29
    specialize le_trans (a + a)
  4. L30
    specialize le_trans (n + n)
  5. L31
    apply le_trans
  6. L32
    exact hcover
  7. L33
    exact hdouble
06Construct an explicit witnessL34–34

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

  1. L34
    exists b
07Separate the logical casesL35–35

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

  1. L35
    split
08Use earlier factsL36–36

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

  1. L36
    exact hprime
09Separate the logical casesL37–37

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

  1. L37
    split
10Use earlier factsL38–39

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

  1. L38
    exact hstrict
  2. L39
    exact hupper

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro hprime
  5. 0005intro hlower
  6. 0006intro hstrict
  7. 0007intro hcover
  8. 0008have hfirst : exists k. k + (a + a) = n + a
  9. 0009specialize add_le_add_right a
  10. 0010specialize add_le_add_right n
  11. 0011specialize add_le_add_right a
  12. 0012apply add_le_add_right
  13. 0013exact hlower
  14. 0014have hsecond : exists k. k + (n + a) = n + n
  15. 0015specialize add_le_add_left a
  16. 0016specialize add_le_add_left n
  17. 0017specialize add_le_add_left n
  18. 0018apply add_le_add_left
  19. 0019exact hlower
  20. 0020have hdouble : exists k. k + (a + a) = n + n
  21. 0021specialize le_trans (a + a)
  22. 0022specialize le_trans (n + a)
  23. 0023specialize le_trans (n + n)
  24. 0024apply le_trans
  25. 0025exact hfirst
  26. 0026exact hsecond
  27. 0027have hupper : exists k. k + b = n + n
  28. 0028specialize le_trans b
  29. 0029specialize le_trans (a + a)
  30. 0030specialize le_trans (n + n)
  31. 0031apply le_trans
  32. 0032exact hcover
  33. 0033exact hdouble
  34. 0034exists b
  35. 0035split
  36. 0036exact hprime
  37. 0037split
  38. 0038exact hstrict
  39. 0039exact hupper