ND0074 · conservative definition

EuclidParametrization

There exist m>n>0 with coprime opposite-parity parameters and c=m²+n², with either ordered leg orientation (m²−n²,2mn) or (2mn,m²−n²).

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

EuclidParametrization(a, b, c)

Exact expansion

exists pi_larger_firstwave pi_smaller_firstwave. ((~((pi_smaller_firstwave) = 0) /\ ((exists pi_gap_firstwave. pi_gap_firstwave + S (pi_smaller_firstwave) = (pi_larger_firstwave)) /\ ((forall pff_divisor_pi_firstwave_coprime. (exists pff_left_pi_firstwave_coprime. (pi_larger_firstwave) = pff_divisor_pi_firstwave_coprime * pff_left_pi_firstwave_coprime) -> (exists pff_right_pi_firstwave_coprime. (pi_smaller_firstwave) = pff_divisor_pi_firstwave_coprime * pff_right_pi_firstwave_coprime) -> pff_divisor_pi_firstwave_coprime = 1) /\ (((((exists pp_even_pi_firstwave_parity_first_even. (pi_larger_firstwave) = 2 * pp_even_pi_firstwave_parity_first_even) /\ (exists pp_odd_pi_firstwave_parity_second_odd. (pi_smaller_firstwave) = 2 * pp_odd_pi_firstwave_parity_second_odd + 1)) \/ ((exists pp_odd_pi_firstwave_parity_first_odd. (pi_larger_firstwave) = 2 * pp_odd_pi_firstwave_parity_first_odd + 1) /\ (exists pp_even_pi_firstwave_parity_second_even. (pi_smaller_firstwave) = 2 * pp_even_pi_firstwave_parity_second_even)))) /\ ((c) = (pi_larger_firstwave) * (pi_larger_firstwave) + (pi_smaller_firstwave) * (pi_smaller_firstwave) /\ (((pi_larger_firstwave) * (pi_larger_firstwave) = (pi_smaller_firstwave) * (pi_smaller_firstwave) + (a) /\ (b) = 2 * ((pi_larger_firstwave) * (pi_smaller_firstwave))) \/ ((pi_larger_firstwave) * (pi_larger_firstwave) = (pi_smaller_firstwave) * (pi_smaller_firstwave) + (b) /\ (a) = 2 * ((pi_larger_firstwave) * (pi_smaller_firstwave))))))))))

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

PD0002 Lt PD0005 Coprime CF0016 OppositeParity

Used by conservative definitions

none

All transitive conservative prerequisites

CF0016 OppositeParity PD0002 Lt PD0003 Dvd PD0005 Coprime PD0009 Even PD0010 Odd

Used by theorem statements or local proof propositions

PF001Z pythagorean_positive_primitive_inverse PF0022 pythagorean_positive_primitive_from_parameters PF0023 pythagorean_positive_primitive_classification

Grand-campaign planning vocabulary

Locate EuclidParametrization in the global campaign vocabulary →

Reviewed EuclidParametrization corresponds to blueprint EuclidParametrization 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.