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.
Statement with defined notation
∀ p. Prime(p) → p = 2 ∨ Mod4One(p) ∨ Mod4Three(p)Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order statement
forall p. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> ((p = 2 \/ exists k. p = 4 * k + 1) \/ exists k. p = 4 * k + 3)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
Read the argument
Proof checkpoints
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 (1)
01Fix variables and assumptionsL1–2
02Establish hclassesL3–6
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mod four trichotomy.
- L3
have hclasses : p = 2 ∨ (Mod4One(p) ∨ Mod4Three(p))Definitions: Mod4One(p)Mod4Three(p)Original native command in the exact edition - L4
specialize prime_mod_four_trichotomy p - L5
apply prime_mod_four_trichotomy - L6
exact hprime
03Separate the logical casesL7–9
04Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
exact hclasses_left
05Separate the logical casesL11–13
06Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact hclasses_right_left
07Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
right
08Use earlier factsL16–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
exact hclasses_right_right
Original defined command ledger · 16 lines
- 0001
intro p - 0002
intro hprime - 0003
have hclasses : p = 2 ∨ (Mod4One(p) ∨ Mod4Three(p))Exact native replay line
have hclasses : (p = 2 \/ ((exists k. p = 4 * k + 1) \/ (exists k. p = 4 * k + 3))) - 0004
specialize prime_mod_four_trichotomy p - 0005
apply prime_mod_four_trichotomy - 0006
exact hprime - 0007
cases hclasses - 0008
left - 0009
left - 0010
exact hclasses_left - 0011
cases hclasses_right - 0012
left - 0013
right - 0014
exact hclasses_right_left - 0015
right - 0016
exact hclasses_right_right