PE0002

least_prime_above_finite_scan

Finite decidable scanning either finds the actual least prime above a or proves every such prime exceeds the scanned interval.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

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.

Every successor is the globally least prime above its predecessor. This is not a sparse Bertrand chain. The bound theorem constructs the list and both power witnesses from k≠0 alone; the separate total-list theorem includes k=0.

Exact theorem in conservative defined notation

∀ a. ∀ n. (∃ x. NextPrime(a,x)) ∨ (∀ x. Prime(x) → Lt(a,x) → Lt(a + n,x))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

NextPrime(a,p) · 1Lt(a,b) · 4Prime(p) · 3

Actual proof prerequisites

prime_decidable · checked external prerequisiteadd_comm · checked external prerequisitele_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall a n. (exists pen_least_scan. ((~(pen_least_scan = 1) /\ forall bpr_left_pc_pen_scan_found_prime bpr_right_pc_pen_scan_found_prime. pen_least_scan = bpr_left_pc_pen_scan_found_prime * bpr_right_pc_pen_scan_found_prime -> bpr_left_pc_pen_scan_found_prime = 1 \/ bpr_right_pc_pen_scan_found_prime = 1)) /\ ((exists pc_lt_pen_scan_found_greater. pc_lt_pen_scan_found_greater + S (a) = (pen_least_scan)) /\ forall pen_comparison_scan_found. ((~(pen_comparison_scan_found = 1) /\ forall bpr_left_pc_pen_scan_found_comparison bpr_right_pc_pen_scan_found_comparison. pen_comparison_scan_found = bpr_left_pc_pen_scan_found_comparison * bpr_right_pc_pen_scan_found_comparison -> bpr_left_pc_pen_scan_found_comparison = 1 \/ bpr_right_pc_pen_scan_found_comparison = 1)) -> (exists pc_lt_pen_scan_found_above. pc_lt_pen_scan_found_above + S (a) = (pen_comparison_scan_found)) -> (exists pc_le_pen_scan_found_minimal. pc_le_pen_scan_found_minimal + (pen_least_scan) = (pen_comparison_scan_found)))) \/ (forall pen_unseen_scan. ((~(pen_unseen_scan = 1) /\ forall bpr_left_pc_pen_scan_prime bpr_right_pc_pen_scan_prime. pen_unseen_scan = bpr_left_pc_pen_scan_prime * bpr_right_pc_pen_scan_prime -> bpr_left_pc_pen_scan_prime = 1 \/ bpr_right_pc_pen_scan_prime = 1)) -> (exists pc_lt_pen_scan_above. pc_lt_pen_scan_above + S (a) = (pen_unseen_scan)) -> (exists pc_lt_pen_scan_unseen. pc_lt_pen_scan_unseen + S (a + n) = (pen_unseen_scan)))

Complete tactic proof in conservative notation

All 57 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

57 script commands · 27 reading checkpoints · 5 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.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro a
02Induction on nL2–2

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

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

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

  1. L3
    right
04Fix variables and assumptionsL4–6

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

  1. L4
    intro q
  2. L5
    intro hp
  3. L6
    intro ha
05Establish hzL7–10

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

  1. L7
    have hz : a + 0 = a
  2. L8
    apply PA3
  3. L9
    rewrite hz
  4. L10
    exact ha
06Separate the logical casesL11–12

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

  1. L11
    cases IH
  2. L12
    left
07Use earlier factsL13–13

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

  1. L13
    exact IH_left
08Establish hdecL14–16

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

  1. L14
    have hdec : Prime(S (a + n)) ∨ ¬Prime(S (a + n))Definitions: Prime(S (a + n))Original native command in the exact edition
  2. L15
    specialize prime_decidable (S (a + n))
  3. L16
    apply prime_decidable
09Separate the logical casesL17–18

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

  1. L17
    cases hdec
  2. L18
    left
10Construct an explicit witnessL19–19

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

  1. L19
    exists S (a + n)
11Separate the logical casesL20–20

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

  1. L20
    split
12Use earlier factsL21–21

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

  1. L21
    exact hdec_left
13Separate the logical casesL22–22

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

  1. L22
    split
14Construct an explicit witnessL23–23

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

  1. L23
    exists n
15Calculate and transport equalitiesL24–25

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

  1. L24
    rewrite PA4
  2. L25
    congr
16Use earlier factsL26–26

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

  1. L26
    apply add_comm
17Fix variables and assumptionsL27–29

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

  1. L27
    intro q
  2. L28
    intro hp
  3. L29
    intro ha
18Use earlier factsL30–33

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

  1. L30
    specialize IH_right q
  2. L31
    apply IH_right
  3. L32
    exact hp
  4. L33
    exact ha
19Separate the logical casesL34–34

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

  1. L34
    right
20Fix variables and assumptionsL35–37

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

  1. L35
    intro q
  2. L36
    intro hp
  3. L37
    intro ha
21Establish hprevL38–42

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

  1. L38
    have hprev : Lt(a + n,q)Definitions: Lt(a + n,q)Original native command in the exact edition
  2. L39
    specialize IH_right q
  3. L40
    apply IH_right
  4. L41
    exact hp
  5. L42
    exact ha
22Establish hcaseL43–47

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

  1. L43
    have hcase : S (a + n) = q ∨ Lt(S (a + n),q)Definitions: Lt(S (a + n),q)Original native command in the exact edition
  2. L44
    specialize le_eq_or_lt (S (a + n))
  3. L45
    specialize le_eq_or_lt q
  4. L46
    apply le_eq_or_lt
  5. L47
    exact hprev
23Separate the logical casesL48–49

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

  1. L48
    cases hcase
  2. L49
    exfalso
24Use earlier factsL50–50

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

  1. L50
    apply hdec_right
25Calculate and transport equalitiesL51–52

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

  1. L51
    rewrite hcase_left
  2. L52
    rewrite hcase_left
26Use earlier factsL53–53

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

  1. L53
    exact hp
27Establish hsuccL54–57

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

  1. L54
    have hsucc : a + S n = S (a + n)
  2. L55
    apply PA4
  3. L56
    rewrite hsucc
  4. L57
    exact hcase_right

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro a
  2. 0002induction n
  3. 0003right
  4. 0004intro q
  5. 0005intro hp
  6. 0006intro ha
  7. 0007have hz : a + 0 = a
  8. 0008apply PA3
  9. 0009rewrite hz
  10. 0010exact ha
  11. 0011cases IH
  12. 0012left
  13. 0013exact IH_left
  14. 0014have hdec : Prime(S (a + n)) ∨ ¬Prime(S (a + n))
  15. 0015specialize prime_decidable (S (a + n))
  16. 0016apply prime_decidable
  17. 0017cases hdec
  18. 0018left
  19. 0019exists S (a + n)
  20. 0020split
  21. 0021exact hdec_left
  22. 0022split
  23. 0023exists n
  24. 0024rewrite PA4
  25. 0025congr
  26. 0026apply add_comm
  27. 0027intro q
  28. 0028intro hp
  29. 0029intro ha
  30. 0030specialize IH_right q
  31. 0031apply IH_right
  32. 0032exact hp
  33. 0033exact ha
  34. 0034right
  35. 0035intro q
  36. 0036intro hp
  37. 0037intro ha
  38. 0038have hprev : Lt(a + n,q)
  39. 0039specialize IH_right q
  40. 0040apply IH_right
  41. 0041exact hp
  42. 0042exact ha
  43. 0043have hcase : S (a + n) = q ∨ Lt(S (a + n),q)
  44. 0044specialize le_eq_or_lt (S (a + n))
  45. 0045specialize le_eq_or_lt q
  46. 0046apply le_eq_or_lt
  47. 0047exact hprev
  48. 0048cases hcase
  49. 0049exfalso
  50. 0050apply hdec_right
  51. 0051rewrite hcase_left
  52. 0052rewrite hcase_left
  53. 0053exact hp
  54. 0054have hsucc : a + S n = S (a + n)
  55. 0055apply PA4
  56. 0056rewrite hsucc
  57. 0057exact hcase_right