PF0022 · theorem body

pythagorean_positive_primitive_from_parameters

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Either canonical Euclidean leg orientation constructs a positive primitive Pythagorean triple with every positivity obligation checked.

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

∀ a. ∀ b. ∀ c. EuclidParametrization(a,b,c) → PrimitiveTriple(a,b,c)

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

ND0069 PrimitiveTriple ND0074 EuclidParametrization

In local proof propositions

CF0016 OppositeParity ND0070 EuclidParameters PD0002 Lt PD0005 Coprime
Exact expanded first-order statement
forall a b c. (exists pi_larger_forward_either pi_smaller_forward_either. ((~((pi_smaller_forward_either) = 0) /\ ((exists pi_gap_forward_either. pi_gap_forward_either + S (pi_smaller_forward_either) = (pi_larger_forward_either)) /\ ((forall pff_divisor_pi_forward_either_coprime. (exists pff_left_pi_forward_either_coprime. (pi_larger_forward_either) = pff_divisor_pi_forward_either_coprime * pff_left_pi_forward_either_coprime) -> (exists pff_right_pi_forward_either_coprime. (pi_smaller_forward_either) = pff_divisor_pi_forward_either_coprime * pff_right_pi_forward_either_coprime) -> pff_divisor_pi_forward_either_coprime = 1) /\ (((((exists pp_even_pi_forward_either_parity_first_even. (pi_larger_forward_either) = 2 * pp_even_pi_forward_either_parity_first_even) /\ (exists pp_odd_pi_forward_either_parity_second_odd. (pi_smaller_forward_either) = 2 * pp_odd_pi_forward_either_parity_second_odd + 1)) \/ ((exists pp_odd_pi_forward_either_parity_first_odd. (pi_larger_forward_either) = 2 * pp_odd_pi_forward_either_parity_first_odd + 1) /\ (exists pp_even_pi_forward_either_parity_second_even. (pi_smaller_forward_either) = 2 * pp_even_pi_forward_either_parity_second_even)))) /\ ((c) = (pi_larger_forward_either) * (pi_larger_forward_either) + (pi_smaller_forward_either) * (pi_smaller_forward_either) /\ (((pi_larger_forward_either) * (pi_larger_forward_either) = (pi_smaller_forward_either) * (pi_smaller_forward_either) + (a) /\ (b) = 2 * ((pi_larger_forward_either) * (pi_smaller_forward_either))) \/ ((pi_larger_forward_either) * (pi_larger_forward_either) = (pi_smaller_forward_either) * (pi_smaller_forward_either) + (b) /\ (a) = 2 * ((pi_larger_forward_either) * (pi_smaller_forward_either))))))))))) -> ((~((a) = 0) /\ (~((b) = 0) /\ (~((c) = 0) /\ ((((a) * (a) + (b) * (b) = (c) * (c)) /\ (forall pff_divisor_pi_forward_triple. (exists pff_left_pi_forward_triple. (a) = pff_divisor_pi_forward_triple * pff_left_pi_forward_triple) -> (exists pff_right_pi_forward_triple. (b) = pff_divisor_pi_forward_triple * pff_right_pi_forward_triple) -> pff_divisor_pi_forward_triple = 1)))))))

Proof neighborhood

Direct theorem prerequisites

PF0021 pythagorean_euclidean_parameters_positive_constructor PF001Y pythagorean_positive_primitive_leg_swap

Direct theorem dependents

PF0023 pythagorean_positive_primitive_classification

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

56 script commands · 27 reading checkpoints · 3 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 (2)
pythagorean euclidean parameters positive constructorpythagorean positive primitive leg swap
01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro hparameters
02Separate the logical casesL5–6

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

  1. L5
    cases hparameters
  2. L6
    cases hparameters_witness
03Establish hpL7–8

Establish this local claim before using it. It is not an additional assumption.

  1. L7
    have hp : ¬x1 = 0 ∧ (Lt(x1,x) ∧ (Coprime(x,x1) ∧ (OppositeParity(x,x1) ∧ (c = x · x + x1 · x1 ∧ (x · x = x1 · x1 + a ∧ b = 2 · (x · x1) ∨ x · x = x1 · x1 + b ∧ a = 2 · (x · x1))))))Definitions: Lt(x1,x)Coprime(x,x1)OppositeParity(x,x1)Original native command in the exact edition
  2. L8
    exact hparameters_witness_witness
04Separate the logical casesL9–14

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

  1. L9
    cases hp
  2. L10
    cases hp_right
  3. L11
    cases hp_right_right
  4. L12
    cases hp_right_right_right
  5. L13
    cases hp_right_right_right_right
  6. L14
    cases hp_right_right_right_right_right
05Establish horientedL15–15

Establish this local claim before using it. It is not an additional assumption.

  1. L15
    have horiented : EuclidParameters(a,b,c,x,x1)Definitions: EuclidParameters(a,b,c,x,x1)Original native command in the exact edition
06Separate the logical casesL16–16

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

  1. L16
    split
07Use earlier factsL17–17

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

  1. L17
    exact hp_left
08Separate the logical casesL18–18

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

  1. L18
    split
09Use earlier factsL19–19

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

  1. L19
    exact hp_right_left
10Separate the logical casesL20–20

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

  1. L20
    split
11Use earlier factsL21–21

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

  1. L21
    exact hp_right_right_left
12Separate the logical casesL22–22

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

  1. L22
    split
13Use earlier factsL23–23

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

  1. L23
    exact hp_right_right_right_left
14Separate the logical casesL24–24

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

  1. L24
    split
15Use earlier factsL25–33

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

  1. L25
    exact hp_right_right_right_right_left
  2. L26
    exact hp_right_right_right_right_right_left
  3. L27
    specialize pythagorean_euclidean_parameters_positive_constructor a
  4. L28
    specialize pythagorean_euclidean_parameters_positive_constructor b
  5. L29
    specialize pythagorean_euclidean_parameters_positive_constructor c
  6. L30
    specialize pythagorean_euclidean_parameters_positive_constructor x
  7. L31
    specialize pythagorean_euclidean_parameters_positive_constructor x1
  8. L32
    apply pythagorean_euclidean_parameters_positive_constructor
  9. L33
    exact horiented
16Establish horientedL34–34

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have horiented : EuclidParameters(b,a,c,x,x1)Definitions: EuclidParameters(b,a,c,x,x1)Original native command in the exact edition
17Separate the logical casesL35–35

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

  1. L35
    split
18Use earlier factsL36–36

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

  1. L36
    exact hp_left
19Separate the logical casesL37–37

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

  1. L37
    split
20Use earlier factsL38–38

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

  1. L38
    exact hp_right_left
21Separate the logical casesL39–39

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

  1. L39
    split
22Use earlier factsL40–40

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

  1. L40
    exact hp_right_right_left
23Separate the logical casesL41–41

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

  1. L41
    split
24Use earlier factsL42–42

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

  1. L42
    exact hp_right_right_right_left
25Separate the logical casesL43–43

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

  1. L43
    split
26Use earlier factsL44–53

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

  1. L44
    exact hp_right_right_right_right_left
  2. L45
    exact hp_right_right_right_right_right_right
  3. L46
    specialize pythagorean_positive_primitive_leg_swap b
  4. L47
    specialize pythagorean_positive_primitive_leg_swap a
  5. L48
    specialize pythagorean_positive_primitive_leg_swap c
  6. L49
    apply pythagorean_positive_primitive_leg_swap
  7. L50
    specialize pythagorean_euclidean_parameters_positive_constructor b
  8. L51
    specialize pythagorean_euclidean_parameters_positive_constructor a
  9. L52
    specialize pythagorean_euclidean_parameters_positive_constructor c
  10. L53
    specialize pythagorean_euclidean_parameters_positive_constructor x
27Use earlier factsL54–56

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

  1. L54
    specialize pythagorean_euclidean_parameters_positive_constructor x1
  2. L55
    apply pythagorean_euclidean_parameters_positive_constructor
  3. L56
    exact horiented

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hparameters
  5. 0005cases hparameters
  6. 0006cases hparameters_witness
  7. 0007have hp : ¬x1 = 0 ∧ (Lt(x1,x) ∧ (Coprime(x,x1) ∧ (OppositeParity(x,x1) ∧ (c = x · x + x1 · x1 ∧ (x · x = x1 · x1 + a ∧ b = 2 · (x · x1) ∨ x · x = x1 · x1 + b ∧ a = 2 · (x · x1))))))
    Exact native replay linehave hp : (~((x1) = 0) /\ ((exists pi_gap_forward_copy. pi_gap_forward_copy + S (x1) = (x)) /\ ((forall pff_divisor_pi_forward_copy_coprime. (exists pff_left_pi_forward_copy_coprime. (x) = pff_divisor_pi_forward_copy_coprime * pff_left_pi_forward_copy_coprime) -> (exists pff_right_pi_forward_copy_coprime. (x1) = pff_divisor_pi_forward_copy_coprime * pff_right_pi_forward_copy_coprime) -> pff_divisor_pi_forward_copy_coprime = 1) /\ (((((exists pp_even_pi_forward_copy_parity_first_even. (x) = 2 * pp_even_pi_forward_copy_parity_first_even) /\ (exists pp_odd_pi_forward_copy_parity_second_odd. (x1) = 2 * pp_odd_pi_forward_copy_parity_second_odd + 1)) \/ ((exists pp_odd_pi_forward_copy_parity_first_odd. (x) = 2 * pp_odd_pi_forward_copy_parity_first_odd + 1) /\ (exists pp_even_pi_forward_copy_parity_second_even. (x1) = 2 * pp_even_pi_forward_copy_parity_second_even)))) /\ ((c) = (x) * (x) + (x1) * (x1) /\ (((x) * (x) = (x1) * (x1) + (a) /\ (b) = 2 * ((x) * (x1))) \/ ((x) * (x) = (x1) * (x1) + (b) /\ (a) = 2 * ((x) * (x1)))))))))
  8. 0008exact hparameters_witness_witness
  9. 0009cases hp
  10. 0010cases hp_right
  11. 0011cases hp_right_right
  12. 0012cases hp_right_right_right
  13. 0013cases hp_right_right_right_right
  14. 0014cases hp_right_right_right_right_right
  15. 0015have horiented : EuclidParameters(a,b,c,x,x1)
    Exact native replay linehave horiented : (~((x1) = 0) /\ ((exists pi_gap_forward_orientation. pi_gap_forward_orientation + S (x1) = (x)) /\ ((forall pff_divisor_pi_forward_orientation_coprime. (exists pff_left_pi_forward_orientation_coprime. (x) = pff_divisor_pi_forward_orientation_coprime * pff_left_pi_forward_orientation_coprime) -> (exists pff_right_pi_forward_orientation_coprime. (x1) = pff_divisor_pi_forward_orientation_coprime * pff_right_pi_forward_orientation_coprime) -> pff_divisor_pi_forward_orientation_coprime = 1) /\ (((((exists pp_even_pi_forward_orientation_parity_first_even. (x) = 2 * pp_even_pi_forward_orientation_parity_first_even) /\ (exists pp_odd_pi_forward_orientation_parity_second_odd. (x1) = 2 * pp_odd_pi_forward_orientation_parity_second_odd + 1)) \/ ((exists pp_odd_pi_forward_orientation_parity_first_odd. (x) = 2 * pp_odd_pi_forward_orientation_parity_first_odd + 1) /\ (exists pp_even_pi_forward_orientation_parity_second_even. (x1) = 2 * pp_even_pi_forward_orientation_parity_second_even)))) /\ ((c) = (x) * (x) + (x1) * (x1) /\ ((x) * (x) = (x1) * (x1) + (a) /\ (b) = 2 * ((x) * (x1))))))))
  16. 0016split
  17. 0017exact hp_left
  18. 0018split
  19. 0019exact hp_right_left
  20. 0020split
  21. 0021exact hp_right_right_left
  22. 0022split
  23. 0023exact hp_right_right_right_left
  24. 0024split
  25. 0025exact hp_right_right_right_right_left
  26. 0026exact hp_right_right_right_right_right_left
  27. 0027specialize pythagorean_euclidean_parameters_positive_constructor a
  28. 0028specialize pythagorean_euclidean_parameters_positive_constructor b
  29. 0029specialize pythagorean_euclidean_parameters_positive_constructor c
  30. 0030specialize pythagorean_euclidean_parameters_positive_constructor x
  31. 0031specialize pythagorean_euclidean_parameters_positive_constructor x1
  32. 0032apply pythagorean_euclidean_parameters_positive_constructor
  33. 0033exact horiented
  34. 0034have horiented : EuclidParameters(b,a,c,x,x1)
    Exact native replay linehave horiented : (~((x1) = 0) /\ ((exists pi_gap_forward_orientation. pi_gap_forward_orientation + S (x1) = (x)) /\ ((forall pff_divisor_pi_forward_orientation_coprime. (exists pff_left_pi_forward_orientation_coprime. (x) = pff_divisor_pi_forward_orientation_coprime * pff_left_pi_forward_orientation_coprime) -> (exists pff_right_pi_forward_orientation_coprime. (x1) = pff_divisor_pi_forward_orientation_coprime * pff_right_pi_forward_orientation_coprime) -> pff_divisor_pi_forward_orientation_coprime = 1) /\ (((((exists pp_even_pi_forward_orientation_parity_first_even. (x) = 2 * pp_even_pi_forward_orientation_parity_first_even) /\ (exists pp_odd_pi_forward_orientation_parity_second_odd. (x1) = 2 * pp_odd_pi_forward_orientation_parity_second_odd + 1)) \/ ((exists pp_odd_pi_forward_orientation_parity_first_odd. (x) = 2 * pp_odd_pi_forward_orientation_parity_first_odd + 1) /\ (exists pp_even_pi_forward_orientation_parity_second_even. (x1) = 2 * pp_even_pi_forward_orientation_parity_second_even)))) /\ ((c) = (x) * (x) + (x1) * (x1) /\ ((x) * (x) = (x1) * (x1) + (b) /\ (a) = 2 * ((x) * (x1))))))))
  35. 0035split
  36. 0036exact hp_left
  37. 0037split
  38. 0038exact hp_right_left
  39. 0039split
  40. 0040exact hp_right_right_left
  41. 0041split
  42. 0042exact hp_right_right_right_left
  43. 0043split
  44. 0044exact hp_right_right_right_right_left
  45. 0045exact hp_right_right_right_right_right_right
  46. 0046specialize pythagorean_positive_primitive_leg_swap b
  47. 0047specialize pythagorean_positive_primitive_leg_swap a
  48. 0048specialize pythagorean_positive_primitive_leg_swap c
  49. 0049apply pythagorean_positive_primitive_leg_swap
  50. 0050specialize pythagorean_euclidean_parameters_positive_constructor b
  51. 0051specialize pythagorean_euclidean_parameters_positive_constructor a
  52. 0052specialize pythagorean_euclidean_parameters_positive_constructor c
  53. 0053specialize pythagorean_euclidean_parameters_positive_constructor x
  54. 0054specialize pythagorean_euclidean_parameters_positive_constructor x1
  55. 0055apply pythagorean_euclidean_parameters_positive_constructor
  56. 0056exact horiented