PF001Z · theorem body

pythagorean_positive_primitive_inverse

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

Every positive primitive ordered Pythagorean triple has positive ordered coprime opposite-parity Euclidean parameters in one of both leg orientations.

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. PrimitiveTriple(a,b,c) → EuclidParametrization(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
Exact expanded first-order statement
forall a b c. ((~((a) = 0) /\ (~((b) = 0) /\ (~((c) = 0) /\ ((((a) * (a) + (b) * (b) = (c) * (c)) /\ (forall pff_divisor_pi_inverse_positive. (exists pff_left_pi_inverse_positive. (a) = pff_divisor_pi_inverse_positive * pff_left_pi_inverse_positive) -> (exists pff_right_pi_inverse_positive. (b) = pff_divisor_pi_inverse_positive * pff_right_pi_inverse_positive) -> pff_divisor_pi_inverse_positive = 1))))))) -> (exists pi_larger_inverse_either pi_smaller_inverse_either. ((~((pi_smaller_inverse_either) = 0) /\ ((exists pi_gap_inverse_either. pi_gap_inverse_either + S (pi_smaller_inverse_either) = (pi_larger_inverse_either)) /\ ((forall pff_divisor_pi_inverse_either_coprime. (exists pff_left_pi_inverse_either_coprime. (pi_larger_inverse_either) = pff_divisor_pi_inverse_either_coprime * pff_left_pi_inverse_either_coprime) -> (exists pff_right_pi_inverse_either_coprime. (pi_smaller_inverse_either) = pff_divisor_pi_inverse_either_coprime * pff_right_pi_inverse_either_coprime) -> pff_divisor_pi_inverse_either_coprime = 1) /\ (((((exists pp_even_pi_inverse_either_parity_first_even. (pi_larger_inverse_either) = 2 * pp_even_pi_inverse_either_parity_first_even) /\ (exists pp_odd_pi_inverse_either_parity_second_odd. (pi_smaller_inverse_either) = 2 * pp_odd_pi_inverse_either_parity_second_odd + 1)) \/ ((exists pp_odd_pi_inverse_either_parity_first_odd. (pi_larger_inverse_either) = 2 * pp_odd_pi_inverse_either_parity_first_odd + 1) /\ (exists pp_even_pi_inverse_either_parity_second_even. (pi_smaller_inverse_either) = 2 * pp_even_pi_inverse_either_parity_second_even)))) /\ ((c) = (pi_larger_inverse_either) * (pi_larger_inverse_either) + (pi_smaller_inverse_either) * (pi_smaller_inverse_either) /\ (((pi_larger_inverse_either) * (pi_larger_inverse_either) = (pi_smaller_inverse_either) * (pi_smaller_inverse_either) + (a) /\ (b) = 2 * ((pi_larger_inverse_either) * (pi_smaller_inverse_either))) \/ ((pi_larger_inverse_either) * (pi_larger_inverse_either) = (pi_smaller_inverse_either) * (pi_smaller_inverse_either) + (b) /\ (a) = 2 * ((pi_larger_inverse_either) * (pi_smaller_inverse_either)))))))))))

Proof neighborhood

Direct theorem prerequisites

PF0014 pythagorean_primitive_legs_opposite_parity PF000C pythagorean_primitive_leg_swap PF001X pythagorean_primitive_odd_even_inverse

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

82 script commands · 36 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 (3)
pythagorean primitive legs opposite paritypythagorean primitive leg swappythagorean primitive odd even inverse
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 hp
02Separate the logical casesL5–7

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

  1. L5
    cases hp
  2. L6
    cases hp_right
  3. L7
    cases hp_right_right
03Establish hparityL8–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean primitive legs opposite parity.

  1. L8
    have hparity : OppositeParity(a,b)Definitions: OppositeParity(a,b)Original native command in the exact edition
  2. L9
    specialize pythagorean_primitive_legs_opposite_parity a
  3. L10
    specialize pythagorean_primitive_legs_opposite_parity b
  4. L11
    specialize pythagorean_primitive_legs_opposite_parity c
  5. L12
    apply pythagorean_primitive_legs_opposite_parity
  6. L13
    exact hp_right_right_right
04Separate the logical casesL14–15

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

  1. L14
    cases hparity
  2. L15
    cases hparity_left
05Establish hparametersL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean primitive odd even inverse.

  1. L16
    have hparameters : ∃ m. ∃ n. EuclidParameters(b,a,c,m,n)Definitions: EuclidParameters(b,a,c,m,n)Original native command in the exact edition
  2. L17
    specialize pythagorean_primitive_odd_even_inverse b
  3. L18
    specialize pythagorean_primitive_odd_even_inverse a
  4. L19
    specialize pythagorean_primitive_odd_even_inverse c
  5. L20
    apply pythagorean_primitive_odd_even_inverse
  6. L21
    specialize pythagorean_primitive_leg_swap a
  7. L22
    specialize pythagorean_primitive_leg_swap b
  8. L23
    specialize pythagorean_primitive_leg_swap c
  9. L24
    apply pythagorean_primitive_leg_swap
  10. L25
    exact hp_right_right_right
06Use earlier factsL26–29

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

  1. L26
    exact hp_right_left
  2. L27
    exact hp_left
  3. L28
    exact hparity_left_right
  4. L29
    exact hparity_left_left
07Separate the logical casesL30–36

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

  1. L30
    cases hparameters
  2. L31
    cases hparameters_witness
  3. L32
    cases hparameters_witness_witness
  4. L33
    cases hparameters_witness_witness_right
  5. L34
    cases hparameters_witness_witness_right_right
  6. L35
    cases hparameters_witness_witness_right_right_right
  7. L36
    cases hparameters_witness_witness_right_right_right_right
08Construct an explicit witnessL37–38

Supply the displayed value, then prove that it has the required property.

  1. L37
    exists x
  2. L38
    exists x1
09Separate the logical casesL39–39

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

  1. L39
    split
10Use earlier factsL40–40

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

  1. L40
    exact hparameters_witness_witness_left
11Separate the logical casesL41–41

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

  1. L41
    split
12Use earlier factsL42–42

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

  1. L42
    exact hparameters_witness_witness_right_left
13Separate the logical casesL43–43

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

  1. L43
    split
14Use earlier factsL44–44

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

  1. L44
    exact hparameters_witness_witness_right_right_left
15Separate the logical casesL45–45

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

  1. L45
    split
16Use earlier factsL46–46

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

  1. L46
    exact hparameters_witness_witness_right_right_right_left
17Separate the logical casesL47–47

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

  1. L47
    split
18Use earlier factsL48–48

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

  1. L48
    exact hparameters_witness_witness_right_right_right_right_left
19Separate the logical casesL49–49

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

  1. L49
    right
20Use earlier factsL50–50

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

  1. L50
    exact hparameters_witness_witness_right_right_right_right_right
21Separate the logical casesL51–51

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

  1. L51
    cases hparity_right
22Establish hparametersL52–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean primitive odd even inverse.

  1. L52
    have hparameters : ∃ m. ∃ n. EuclidParameters(a,b,c,m,n)Definitions: EuclidParameters(a,b,c,m,n)Original native command in the exact edition
  2. L53
    specialize pythagorean_primitive_odd_even_inverse a
  3. L54
    specialize pythagorean_primitive_odd_even_inverse b
  4. L55
    specialize pythagorean_primitive_odd_even_inverse c
  5. L56
    apply pythagorean_primitive_odd_even_inverse
  6. L57
    exact hp_right_right_right
  7. L58
    exact hp_left
  8. L59
    exact hp_right_left
  9. L60
    exact hparity_right_left
  10. L61
    exact hparity_right_right
23Separate the logical casesL62–68

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

  1. L62
    cases hparameters
  2. L63
    cases hparameters_witness
  3. L64
    cases hparameters_witness_witness
  4. L65
    cases hparameters_witness_witness_right
  5. L66
    cases hparameters_witness_witness_right_right
  6. L67
    cases hparameters_witness_witness_right_right_right
  7. L68
    cases hparameters_witness_witness_right_right_right_right
24Construct an explicit witnessL69–70

Supply the displayed value, then prove that it has the required property.

  1. L69
    exists x
  2. L70
    exists x1
25Separate the logical casesL71–71

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

  1. L71
    split
26Use earlier factsL72–72

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

  1. L72
    exact hparameters_witness_witness_left
27Separate the logical casesL73–73

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

  1. L73
    split
28Use earlier factsL74–74

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

  1. L74
    exact hparameters_witness_witness_right_left
29Separate the logical casesL75–75

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

  1. L75
    split
30Use earlier factsL76–76

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

  1. L76
    exact hparameters_witness_witness_right_right_left
31Separate the logical casesL77–77

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

  1. L77
    split
32Use earlier factsL78–78

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

  1. L78
    exact hparameters_witness_witness_right_right_right_left
33Separate the logical casesL79–79

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

  1. L79
    split
34Use earlier factsL80–80

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

  1. L80
    exact hparameters_witness_witness_right_right_right_right_left
35Separate the logical casesL81–81

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

  1. L81
    left
36Use earlier factsL82–82

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

  1. L82
    exact hparameters_witness_witness_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hp
  5. 0005cases hp
  6. 0006cases hp_right
  7. 0007cases hp_right_right
  8. 0008have hparity : OppositeParity(a,b)
    Exact native replay linehave hparity : (((exists pp_even_pi_inverse_choice_first_even. (a) = 2 * pp_even_pi_inverse_choice_first_even) /\ (exists pp_odd_pi_inverse_choice_second_odd. (b) = 2 * pp_odd_pi_inverse_choice_second_odd + 1)) \/ ((exists pp_odd_pi_inverse_choice_first_odd. (a) = 2 * pp_odd_pi_inverse_choice_first_odd + 1) /\ (exists pp_even_pi_inverse_choice_second_even. (b) = 2 * pp_even_pi_inverse_choice_second_even)))
  9. 0009specialize pythagorean_primitive_legs_opposite_parity a
  10. 0010specialize pythagorean_primitive_legs_opposite_parity b
  11. 0011specialize pythagorean_primitive_legs_opposite_parity c
  12. 0012apply pythagorean_primitive_legs_opposite_parity
  13. 0013exact hp_right_right_right
  14. 0014cases hparity
  15. 0015cases hparity_left
  16. 0016have hparameters : ∃ m. ∃ n. EuclidParameters(b,a,c,m,n)
    Exact native replay linehave hparameters : exists m n. ((~((n) = 0) /\ ((exists pi_gap_choice. pi_gap_choice + S (n) = (m)) /\ ((forall pff_divisor_pi_choice_coprime. (exists pff_left_pi_choice_coprime. (m) = pff_divisor_pi_choice_coprime * pff_left_pi_choice_coprime) -> (exists pff_right_pi_choice_coprime. (n) = pff_divisor_pi_choice_coprime * pff_right_pi_choice_coprime) -> pff_divisor_pi_choice_coprime = 1) /\ (((((exists pp_even_pi_choice_parity_first_even. (m) = 2 * pp_even_pi_choice_parity_first_even) /\ (exists pp_odd_pi_choice_parity_second_odd. (n) = 2 * pp_odd_pi_choice_parity_second_odd + 1)) \/ ((exists pp_odd_pi_choice_parity_first_odd. (m) = 2 * pp_odd_pi_choice_parity_first_odd + 1) /\ (exists pp_even_pi_choice_parity_second_even. (n) = 2 * pp_even_pi_choice_parity_second_even)))) /\ ((c) = (m) * (m) + (n) * (n) /\ ((m) * (m) = (n) * (n) + (b) /\ (a) = 2 * ((m) * (n)))))))))
  17. 0017specialize pythagorean_primitive_odd_even_inverse b
  18. 0018specialize pythagorean_primitive_odd_even_inverse a
  19. 0019specialize pythagorean_primitive_odd_even_inverse c
  20. 0020apply pythagorean_primitive_odd_even_inverse
  21. 0021specialize pythagorean_primitive_leg_swap a
  22. 0022specialize pythagorean_primitive_leg_swap b
  23. 0023specialize pythagorean_primitive_leg_swap c
  24. 0024apply pythagorean_primitive_leg_swap
  25. 0025exact hp_right_right_right
  26. 0026exact hp_right_left
  27. 0027exact hp_left
  28. 0028exact hparity_left_right
  29. 0029exact hparity_left_left
  30. 0030cases hparameters
  31. 0031cases hparameters_witness
  32. 0032cases hparameters_witness_witness
  33. 0033cases hparameters_witness_witness_right
  34. 0034cases hparameters_witness_witness_right_right
  35. 0035cases hparameters_witness_witness_right_right_right
  36. 0036cases hparameters_witness_witness_right_right_right_right
  37. 0037exists x
  38. 0038exists x1
  39. 0039split
  40. 0040exact hparameters_witness_witness_left
  41. 0041split
  42. 0042exact hparameters_witness_witness_right_left
  43. 0043split
  44. 0044exact hparameters_witness_witness_right_right_left
  45. 0045split
  46. 0046exact hparameters_witness_witness_right_right_right_left
  47. 0047split
  48. 0048exact hparameters_witness_witness_right_right_right_right_left
  49. 0049right
  50. 0050exact hparameters_witness_witness_right_right_right_right_right
  51. 0051cases hparity_right
  52. 0052have hparameters : ∃ m. ∃ n. EuclidParameters(a,b,c,m,n)
    Exact native replay linehave hparameters : exists m n. ((~((n) = 0) /\ ((exists pi_gap_choice. pi_gap_choice + S (n) = (m)) /\ ((forall pff_divisor_pi_choice_coprime. (exists pff_left_pi_choice_coprime. (m) = pff_divisor_pi_choice_coprime * pff_left_pi_choice_coprime) -> (exists pff_right_pi_choice_coprime. (n) = pff_divisor_pi_choice_coprime * pff_right_pi_choice_coprime) -> pff_divisor_pi_choice_coprime = 1) /\ (((((exists pp_even_pi_choice_parity_first_even. (m) = 2 * pp_even_pi_choice_parity_first_even) /\ (exists pp_odd_pi_choice_parity_second_odd. (n) = 2 * pp_odd_pi_choice_parity_second_odd + 1)) \/ ((exists pp_odd_pi_choice_parity_first_odd. (m) = 2 * pp_odd_pi_choice_parity_first_odd + 1) /\ (exists pp_even_pi_choice_parity_second_even. (n) = 2 * pp_even_pi_choice_parity_second_even)))) /\ ((c) = (m) * (m) + (n) * (n) /\ ((m) * (m) = (n) * (n) + (a) /\ (b) = 2 * ((m) * (n)))))))))
  53. 0053specialize pythagorean_primitive_odd_even_inverse a
  54. 0054specialize pythagorean_primitive_odd_even_inverse b
  55. 0055specialize pythagorean_primitive_odd_even_inverse c
  56. 0056apply pythagorean_primitive_odd_even_inverse
  57. 0057exact hp_right_right_right
  58. 0058exact hp_left
  59. 0059exact hp_right_left
  60. 0060exact hparity_right_left
  61. 0061exact hparity_right_right
  62. 0062cases hparameters
  63. 0063cases hparameters_witness
  64. 0064cases hparameters_witness_witness
  65. 0065cases hparameters_witness_witness_right
  66. 0066cases hparameters_witness_witness_right_right
  67. 0067cases hparameters_witness_witness_right_right_right
  68. 0068cases hparameters_witness_witness_right_right_right_right
  69. 0069exists x
  70. 0070exists x1
  71. 0071split
  72. 0072exact hparameters_witness_witness_left
  73. 0073split
  74. 0074exact hparameters_witness_witness_right_left
  75. 0075split
  76. 0076exact hparameters_witness_witness_right_right_left
  77. 0077split
  78. 0078exact hparameters_witness_witness_right_right_right_left
  79. 0079split
  80. 0080exact hparameters_witness_witness_right_right_right_right_left
  81. 0081left
  82. 0082exact hparameters_witness_witness_right_right_right_right_right