TF000D

three_mod_four_prime_divisor_exists

Every natural congruent to three modulo four has an actual prime divisor congruent to three modulo four, obtained by constructive finite search and beta-coded prime factorization.

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

∀ n. Mod4Three(n) → ∃ x. PrimeThreeModFourDivisor(n,x)

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

Definition DAG

PrimeThreeModFourDivisor(n,p) · 1Mod4Three(n) · 1

Actual proof prerequisites

three_mod_four_progression_nonzerothree_mod_four_prime_divisor_bounded_searchpositive_number_with_admissible_prime_divisors_is_two_squareprime_mod_four_good_or_three · checked external prerequisitedivisor_le_nonzero · checked external prerequisitethree_mod_four_progression_not_two_square
Original expanded first-order statement 
forall n. (exists ff_residue_ptmf_number. (n) = 4 * ff_residue_ptmf_number + 3) -> exists p. ((((~(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 46 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

46 script commands · 16 reading checkpoints · 3 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 (4)
three mod four progression nonzerothree mod four prime divisor bounded searchpositive number with admissible prime divisors is two squarethree mod four progression not two square
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro hthree
02Establish hnonzeroL3–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply three mod four progression nonzero.

  1. L3
    have hnonzero : ~(n = 0)
  2. L4
    intro hzero
  3. L5
    specialize three_mod_four_progression_nonzero n
  4. L6
    apply three_mod_four_progression_nonzero
  5. L7
    exact hthree
  6. L8
    exact hzero
  7. L9
    specialize three_mod_four_prime_divisor_bounded_search n
  8. L10
    specialize three_mod_four_prime_divisor_bounded_search n
03Separate the logical casesL11–12

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

  1. L11
    cases three_mod_four_prime_divisor_bounded_search
  2. L12
    exfalso
04Establish hrepresentedL13–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply positive number with admissible prime divisors is two square.

  1. L13
    have hrepresented : exists ptmf_first_represented ptmf_second_represented. (n) = ptmf_first_represented * ptmf_first_represented + ptmf_second_represented * ptmf_second_represented
  2. L14
    specialize positive_number_with_admissible_prime_divisors_is_two_square n
  3. L15
    apply positive_number_with_admissible_prime_divisors_is_two_square
  4. L16
    exact hnonzero
  5. L17
    intro p
  6. L18
    intro hprime
  7. L19
    intro hdivides
05Establish hclassL20–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mod four good or three.

  1. L20
    have hclass : (p = 2 \/ exists k. p = 4 * k + 1) \/ exists k. p = 4 * k + 3
  2. L21
    specialize prime_mod_four_good_or_three p
  3. L22
    apply prime_mod_four_good_or_three
  4. L23
    exact hprime
06Separate the logical casesL24–24

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

  1. L24
    cases hclass
07Use earlier factsL25–25

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

  1. L25
    exact hclass_left
08Separate the logical casesL26–26

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

  1. L26
    exfalso
09Use earlier factsL27–33

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

  1. L27
    specialize three_mod_four_prime_divisor_bounded_search_left p
  2. L28
    apply three_mod_four_prime_divisor_bounded_search_left
  3. L29
    specialize divisor_le_nonzero p
  4. L30
    specialize divisor_le_nonzero n
  5. L31
    apply divisor_le_nonzero
  6. L32
    exact hnonzero
  7. L33
    exact hdivides
10Separate the logical casesL34–34

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

  1. L34
    split
11Use earlier factsL35–35

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

  1. L35
    exact hprime
12Separate the logical casesL36–36

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

  1. L36
    split
13Use earlier factsL37–42

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

  1. L37
    exact hclass_right
  2. L38
    exact hdivides
  3. L39
    specialize three_mod_four_progression_not_two_square n
  4. L40
    apply three_mod_four_progression_not_two_square
  5. L41
    exact hthree
  6. L42
    exact hrepresented
14Separate the logical casesL43–44

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

  1. L43
    cases three_mod_four_prime_divisor_bounded_search_right
  2. L44
    cases three_mod_four_prime_divisor_bounded_search_right_witness
15Construct an explicit witnessL45–45

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

  1. L45
    exists x
16Use earlier factsL46–46

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

  1. L46
    exact three_mod_four_prime_divisor_bounded_search_right_witness_right

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro n
  2. 0002intro hthree
  3. 0003have hnonzero : ~(n = 0)
  4. 0004intro hzero
  5. 0005specialize three_mod_four_progression_nonzero n
  6. 0006apply three_mod_four_progression_nonzero
  7. 0007exact hthree
  8. 0008exact hzero
  9. 0009specialize three_mod_four_prime_divisor_bounded_search n
  10. 0010specialize three_mod_four_prime_divisor_bounded_search n
  11. 0011cases three_mod_four_prime_divisor_bounded_search
  12. 0012exfalso
  13. 0013have hrepresented : exists ptmf_first_represented ptmf_second_represented. (n) = ptmf_first_represented * ptmf_first_represented + ptmf_second_represented * ptmf_second_represented
  14. 0014specialize positive_number_with_admissible_prime_divisors_is_two_square n
  15. 0015apply positive_number_with_admissible_prime_divisors_is_two_square
  16. 0016exact hnonzero
  17. 0017intro p
  18. 0018intro hprime
  19. 0019intro hdivides
  20. 0020have hclass : (p = 2 \/ exists k. p = 4 * k + 1) \/ exists k. p = 4 * k + 3
  21. 0021specialize prime_mod_four_good_or_three p
  22. 0022apply prime_mod_four_good_or_three
  23. 0023exact hprime
  24. 0024cases hclass
  25. 0025exact hclass_left
  26. 0026exfalso
  27. 0027specialize three_mod_four_prime_divisor_bounded_search_left p
  28. 0028apply three_mod_four_prime_divisor_bounded_search_left
  29. 0029specialize divisor_le_nonzero p
  30. 0030specialize divisor_le_nonzero n
  31. 0031apply divisor_le_nonzero
  32. 0032exact hnonzero
  33. 0033exact hdivides
  34. 0034split
  35. 0035exact hprime
  36. 0036split
  37. 0037exact hclass_right
  38. 0038exact hdivides
  39. 0039specialize three_mod_four_progression_not_two_square n
  40. 0040apply three_mod_four_progression_not_two_square
  41. 0041exact hthree
  42. 0042exact hrepresented
  43. 0043cases three_mod_four_prime_divisor_bounded_search_right
  44. 0044cases three_mod_four_prime_divisor_bounded_search_right_witness
  45. 0045exists x
  46. 0046exact three_mod_four_prime_divisor_bounded_search_right_witness_right