TF000B

three_mod_four_prime_divisor_decidable

For every candidate and dividend, actual three-mod-four prime divisibility is constructively decidable.

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

∀ p. ∀ n. PrimeThreeModFourDivisor(n,p) ∨ ¬PrimeThreeModFourDivisor(n,p)

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

Definition DAG

PrimeThreeModFourDivisor(n,p) · 2

Actual proof prerequisites

prime_divides_decidable · checked external prerequisiteprime_mod_four_good_or_three · checked external prerequisitethree_mod_four_good_prime_exclusive
Original expanded first-order statement 
forall p n. (((((~(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)))) \/ ~((((~(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 34 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

34 script commands · 18 reading checkpoints · 1 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 good prime exclusive
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro n
02Use earlier factsL3–4

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

  1. L3
    specialize prime_divides_decidable p
  2. L4
    specialize prime_divides_decidable n
03Separate the logical casesL5–6

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

  1. L5
    cases prime_divides_decidable
  2. L6
    cases prime_divides_decidable_left
04Establish hclassL7–10

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. L7
    have hclass : (p = 2 \/ exists k. p = 4 * k + 1) \/ exists k. p = 4 * k + 3
  2. L8
    specialize prime_mod_four_good_or_three p
  3. L9
    apply prime_mod_four_good_or_three
  4. L10
    exact prime_divides_decidable_left_left
05Separate the logical casesL11–12

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

  1. L11
    cases hclass
  2. L12
    right
06Fix variables and assumptionsL13–13

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

  1. L13
    intro hbad
07Separate the logical casesL14–15

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

  1. L14
    cases hbad
  2. L15
    cases hbad_right
08Use earlier factsL16–20

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

  1. L16
    specialize three_mod_four_good_prime_exclusive p
  2. L17
    apply three_mod_four_good_prime_exclusive
  3. L18
    exact prime_divides_decidable_left_left
  4. L19
    exact hclass_left
  5. L20
    exact hbad_right_left
09Separate the logical casesL21–22

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

  1. L21
    left
  2. L22
    split
10Use earlier factsL23–23

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

  1. L23
    exact prime_divides_decidable_left_left
11Separate the logical casesL24–24

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

  1. L24
    split
12Use earlier factsL25–26

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

  1. L25
    exact hclass_right
  2. L26
    exact prime_divides_decidable_left_right
13Separate the logical casesL27–27

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

  1. L27
    right
14Fix variables and assumptionsL28–28

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

  1. L28
    intro hbad
15Separate the logical casesL29–30

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

  1. L29
    cases hbad
  2. L30
    cases hbad_right
16Use earlier factsL31–31

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

  1. L31
    apply prime_divides_decidable_right
17Separate the logical casesL32–32

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

  1. L32
    split
18Use earlier factsL33–34

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

  1. L33
    exact hbad_left
  2. L34
    exact hbad_right_right

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003specialize prime_divides_decidable p
  4. 0004specialize prime_divides_decidable n
  5. 0005cases prime_divides_decidable
  6. 0006cases prime_divides_decidable_left
  7. 0007have hclass : (p = 2 \/ exists k. p = 4 * k + 1) \/ exists k. p = 4 * k + 3
  8. 0008specialize prime_mod_four_good_or_three p
  9. 0009apply prime_mod_four_good_or_three
  10. 0010exact prime_divides_decidable_left_left
  11. 0011cases hclass
  12. 0012right
  13. 0013intro hbad
  14. 0014cases hbad
  15. 0015cases hbad_right
  16. 0016specialize three_mod_four_good_prime_exclusive p
  17. 0017apply three_mod_four_good_prime_exclusive
  18. 0018exact prime_divides_decidable_left_left
  19. 0019exact hclass_left
  20. 0020exact hbad_right_left
  21. 0021left
  22. 0022split
  23. 0023exact prime_divides_decidable_left_left
  24. 0024split
  25. 0025exact hclass_right
  26. 0026exact prime_divides_decidable_left_right
  27. 0027right
  28. 0028intro hbad
  29. 0029cases hbad
  30. 0030cases hbad_right
  31. 0031apply prime_divides_decidable_right
  32. 0032split
  33. 0033exact hbad_left
  34. 0034exact hbad_right_right