TF000C

three_mod_four_prime_divisor_bounded_search

Finite induction either excludes every three-mod-four prime divisor up to the supplied bound or returns an actual bounded prime-divisor witness.

Alpha v34 checked-use · first admitted v23 · 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.

The exact G025 progression-prime milestone is fully proved in unchanged constructive arithmetic; Mod4Three deliberately reuses its existing Quadratic Reciprocity definition PD0012. The much stronger full Dirichlet progression-prime milestone G030 remains open.

Exact theorem in conservative defined notation

∀ B. ∀ n. (∀ x. Le(x,B) → ¬PrimeThreeModFourDivisor(n,x)) ∨ (∃ x. Le(x,B) ∧ PrimeThreeModFourDivisor(n,x))

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

Definition DAG

PrimeThreeModFourDivisor(n,p) · 2Le(a,b) · 2

Actual proof prerequisites

le_zero · checked external prerequisiteprime_nonzero · checked external prerequisitethree_mod_four_prime_divisor_decidablele_refl · checked external prerequisitele_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisitele_succ · checked external prerequisite
Original expanded first-order statement 
forall B n. ((forall p. (exists ptmf_gap_search. ptmf_gap_search + p = B) -> ~((((~(p = 1) /\ forall frm_prime_left_ptmf_source_prime frm_prime_right_ptmf_source_prime. p = frm_prime_left_ptmf_source_prime * frm_prime_right_ptmf_source_prime -> frm_prime_left_ptmf_source_prime = 1 \/ frm_prime_right_ptmf_source_prime = 1)) /\ ((exists ff_residue_ptmf_source_residue. (p) = 4 * ff_residue_ptmf_source_residue + 3) /\ (exists ff_quotient_ptmf_source_divides. (n) = (p) * ff_quotient_ptmf_source_divides))))) \/ (exists p. ((exists ptmf_gap_search. ptmf_gap_search + p = B) /\ ((((~(p = 1) /\ forall frm_prime_left_ptmf_source_prime frm_prime_right_ptmf_source_prime. p = frm_prime_left_ptmf_source_prime * frm_prime_right_ptmf_source_prime -> frm_prime_left_ptmf_source_prime = 1 \/ frm_prime_right_ptmf_source_prime = 1)) /\ ((exists ff_residue_ptmf_source_residue. (p) = 4 * ff_residue_ptmf_source_residue + 3) /\ (exists ff_quotient_ptmf_source_divides. (n) = (p) * ff_quotient_ptmf_source_divides)))))))

Complete unchanged native tactic proof

All 66 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

66 script commands · 24 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 (1)
three mod four prime divisor decidable
01Induction on BL1–2

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

  1. L1
    induction B
  2. L2
    intro n
02Separate the logical casesL3–3

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

  1. L3
    left
03Fix variables and assumptionsL4–6

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

  1. L4
    intro p
  2. L5
    intro hbound
  3. L6
    intro hbad
04Separate the logical casesL7–7

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

  1. L7
    cases hbad
05Establish hpzeroL8–17

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

  1. L8
    have hpzero : p = 0
  2. L9
    specialize le_zero p
  3. L10
    apply le_zero
  4. L11
    exact hbound
  5. L12
    specialize prime_nonzero p
  6. L13
    apply prime_nonzero
  7. L14
    exact hbad_left
  8. L15
    exact hpzero
  9. L16
    intro n
  10. L17
    specialize three_mod_four_prime_divisor_decidable (S B)
06Use earlier factsL18–18

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

  1. L18
    specialize three_mod_four_prime_divisor_decidable n
07Separate the logical casesL19–20

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

  1. L19
    cases three_mod_four_prime_divisor_decidable
  2. L20
    right
08Construct an explicit witnessL21–21

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

  1. L21
    exists S B
09Separate the logical casesL22–22

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

  1. L22
    split
10Use earlier factsL23–26

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

  1. L23
    specialize le_refl (S B)
  2. L24
    exact le_refl
  3. L25
    exact three_mod_four_prime_divisor_decidable_left
  4. L26
    specialize IH n
11Separate the logical casesL27–28

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

  1. L27
    cases IH
  2. L28
    left
12Fix variables and assumptionsL29–31

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

  1. L29
    intro p
  2. L30
    intro hbound
  3. L31
    intro hbad
13Establish hsplitL32–36

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

  1. L32
    have hsplit : p = S B \/ exists h. h + S p = S B
  2. L33
    specialize le_eq_or_lt p
  3. L34
    specialize le_eq_or_lt (S B)
  4. L35
    apply le_eq_or_lt
  5. L36
    exact hbound
14Separate the logical casesL37–39

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

  1. L37
    cases hsplit
  2. L38
    cases hbad
  3. L39
    cases hbad_right
15Calculate and transport equalitiesL40–43

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

  1. L40
    rewrite hsplit_left at hbad_left
  2. L41
    rewrite hsplit_left at hbad_left
  3. L42
    rewrite hsplit_left at hbad_right_left
  4. L43
    rewrite hsplit_left at hbad_right_right
16Use earlier factsL44–44

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

  1. L44
    apply three_mod_four_prime_divisor_decidable_right
17Separate the logical casesL45–45

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

  1. L45
    split
18Use earlier factsL46–46

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

  1. L46
    exact hbad_left
19Separate the logical casesL47–47

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

  1. L47
    split
20Use earlier factsL48–56

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

  1. L48
    exact hbad_right_left
  2. L49
    exact hbad_right_right
  3. L50
    specialize IH_left p
  4. L51
    apply IH_left
  5. L52
    specialize le_of_succ_le_succ p
  6. L53
    specialize le_of_succ_le_succ B
  7. L54
    apply le_of_succ_le_succ
  8. L55
    exact hsplit_right
  9. L56
    exact hbad
21Separate the logical casesL57–59

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

  1. L57
    right
  2. L58
    cases IH_right
  3. L59
    cases IH_right_witness
22Construct an explicit witnessL60–60

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

  1. L60
    exists x
23Separate the logical casesL61–61

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

  1. L61
    split
24Use earlier factsL62–66

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

  1. L62
    specialize le_succ x
  2. L63
    specialize le_succ B
  3. L64
    apply le_succ
  4. L65
    exact IH_right_witness_left
  5. L66
    exact IH_right_witness_right

Library-wide reading audit

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