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
∀ m. ∀ n. ∀ d. m · m = n · n + d → Coprime(m,n) → OppositeParity(m,n) → PrimitivePythagorean(d,2 · (m · n),m · m + n · n)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 m n d. m * m = n * n + d -> (forall pff_divisor_primitive_parameters. (exists pff_left_primitive_parameters. (m) = pff_divisor_primitive_parameters * pff_left_primitive_parameters) -> (exists pff_right_primitive_parameters. (n) = pff_divisor_primitive_parameters * pff_right_primitive_parameters) -> pff_divisor_primitive_parameters = 1) -> ((((exists pp_even_primitive_parameters_first_even. (m) = 2 * pp_even_primitive_parameters_first_even) /\ (exists pp_odd_primitive_parameters_second_odd. (n) = 2 * pp_odd_primitive_parameters_second_odd + 1)) \/ ((exists pp_odd_primitive_parameters_first_odd. (m) = 2 * pp_odd_primitive_parameters_first_odd + 1) /\ (exists pp_even_primitive_parameters_second_even. (n) = 2 * pp_even_primitive_parameters_second_even)))) -> ((((d) * (d) + (2 * (m * n)) * (2 * (m * n)) = (m * m + n * n) * (m * m + n * n)) /\ (forall pff_divisor_euclidean_result. (exists pff_left_euclidean_result. (d) = pff_divisor_euclidean_result * pff_left_euclidean_result) -> (exists pff_right_euclidean_result. (2 * (m * n)) = pff_divisor_euclidean_result * pff_right_euclidean_result) -> pff_divisor_euclidean_result = 1)))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 (2)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–7
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L7
split
03Use earlier factsL8–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L8
specialize pythagorean_euclidean_identity m - L9
specialize pythagorean_euclidean_identity n - L10
specialize pythagorean_euclidean_identity d - L11
apply pythagorean_euclidean_identity - L12
exact hgap - L13
specialize pythagorean_primitive_euclidean_legs m - L14
specialize pythagorean_primitive_euclidean_legs n - L15
specialize pythagorean_primitive_euclidean_legs d - L16
apply pythagorean_primitive_euclidean_legs - L17
exact hgap
Original defined command ledger · 19 lines
- 0001
intro m - 0002
intro n - 0003
intro d - 0004
intro hgap - 0005
intro hcoprime - 0006
intro hopposite - 0007
split - 0008
specialize pythagorean_euclidean_identity m - 0009
specialize pythagorean_euclidean_identity n - 0010
specialize pythagorean_euclidean_identity d - 0011
apply pythagorean_euclidean_identity - 0012
exact hgap - 0013
specialize pythagorean_primitive_euclidean_legs m - 0014
specialize pythagorean_primitive_euclidean_legs n - 0015
specialize pythagorean_primitive_euclidean_legs d - 0016
apply pythagorean_primitive_euclidean_legs - 0017
exact hgap - 0018
exact hcoprime - 0019
exact hopposite