ND0069 · conservative definition

PrimitiveTriple

Exactly the blueprint's positive primitive ordered triple: all three coordinates are nonzero, the square equation holds, and the legs are coprime.

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.

Readable signature

PrimitiveTriple(a, b, c)

Exact expansion

(~((a) = 0) /\ (~((b) = 0) /\ (~((c) = 0) /\ ((((a) * (a) + (b) * (b) = (c) * (c)) /\ (forall pff_divisor_pi_firstwave. (exists pff_left_pi_firstwave. (a) = pff_divisor_pi_firstwave * pff_left_pi_firstwave) -> (exists pff_right_pi_firstwave. (b) = pff_divisor_pi_firstwave * pff_right_pi_firstwave) -> pff_divisor_pi_firstwave = 1))))))

This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

CF0013 PrimitivePythagorean

Used by conservative definitions

none

All transitive conservative prerequisites

CF0011 Pythagorean CF0013 PrimitivePythagorean PD0003 Dvd PD0005 Coprime

Used by theorem statements or local proof propositions

PF001Y pythagorean_positive_primitive_leg_swap PF001Z pythagorean_positive_primitive_inverse PF0021 pythagorean_euclidean_parameters_positive_constructor PF0022 pythagorean_positive_primitive_from_parameters PF0023 pythagorean_positive_primitive_classification

Grand-campaign planning vocabulary

Locate PrimitiveTriple in the global campaign vocabulary →

Reviewed PrimitiveTriple corresponds to blueprint PrimitiveTriple with checked argument positions [0, 1, 2].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.