PF0021 · theorem body

pythagorean_euclidean_parameters_positive_constructor

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

The checked Euclidean constructor, strengthened with real positivity, supplies exactly the positive primitive triple used in the classification.

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. ∀ m. ∀ n. EuclidParameters(a,b,c,m,n) → 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 ND0070 EuclidParameters

In local proof propositions

none
Exact expanded first-order statement
forall a b c m n. ((~((n) = 0) /\ ((exists pi_gap_forward_parameters. pi_gap_forward_parameters + S (n) = (m)) /\ ((forall pff_divisor_pi_forward_parameters_coprime. (exists pff_left_pi_forward_parameters_coprime. (m) = pff_divisor_pi_forward_parameters_coprime * pff_left_pi_forward_parameters_coprime) -> (exists pff_right_pi_forward_parameters_coprime. (n) = pff_divisor_pi_forward_parameters_coprime * pff_right_pi_forward_parameters_coprime) -> pff_divisor_pi_forward_parameters_coprime = 1) /\ (((((exists pp_even_pi_forward_parameters_parity_first_even. (m) = 2 * pp_even_pi_forward_parameters_parity_first_even) /\ (exists pp_odd_pi_forward_parameters_parity_second_odd. (n) = 2 * pp_odd_pi_forward_parameters_parity_second_odd + 1)) \/ ((exists pp_odd_pi_forward_parameters_parity_first_odd. (m) = 2 * pp_odd_pi_forward_parameters_parity_first_odd + 1) /\ (exists pp_even_pi_forward_parameters_parity_second_even. (n) = 2 * pp_even_pi_forward_parameters_parity_second_even)))) /\ ((c) = (m) * (m) + (n) * (n) /\ ((m) * (m) = (n) * (n) + (a) /\ (b) = 2 * ((m) * (n))))))))) -> ((~((a) = 0) /\ (~((b) = 0) /\ (~((c) = 0) /\ ((((a) * (a) + (b) * (b) = (c) * (c)) /\ (forall pff_divisor_pi_forward_positive. (exists pff_left_pi_forward_positive. (a) = pff_divisor_pi_forward_positive * pff_left_pi_forward_positive) -> (exists pff_right_pi_forward_positive. (b) = pff_divisor_pi_forward_positive * pff_right_pi_forward_positive) -> pff_divisor_pi_forward_positive = 1)))))))

Proof neighborhood

Direct theorem prerequisites

PF0020 pythagorean_ordered_gap_positive PF000T pythagorean_primitive_euclidean_constructor PF000A pythagorean_hypotenuse_nonzero mul_ne_zero · Stable closed succ_ne_zero · Stable closed

Direct theorem dependents

PF0022 pythagorean_positive_primitive_from_parameters

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

62 script commands · 16 reading checkpoints · 2 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 ordered gap positivepythagorean primitive euclidean constructorpythagorean hypotenuse nonzero
01Fix variables and assumptionsL1–6

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 m
  5. L5
    intro n
  6. L6
    intro hp
02Separate the logical casesL7–12

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

  1. L7
    cases hp
  2. L8
    cases hp_right
  3. L9
    cases hp_right_right
  4. L10
    cases hp_right_right_right
  5. L11
    cases hp_right_right_right_right
  6. L12
    cases hp_right_right_right_right_right
03Establish hpositiveL13–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean ordered gap positive.

  1. L13
    have hpositive : ~(m = 0) /\ ~(a = 0)
  2. L14
    specialize pythagorean_ordered_gap_positive a
  3. L15
    specialize pythagorean_ordered_gap_positive m
  4. L16
    specialize pythagorean_ordered_gap_positive n
  5. L17
    apply pythagorean_ordered_gap_positive
  6. L18
    exact hp_left
  7. L19
    exact hp_right_left
  8. L20
    exact hp_right_right_right_right_right_left
04Separate the logical casesL21–22

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

  1. L21
    cases hpositive
  2. L22
    split
05Use earlier factsL23–23

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

  1. L23
    exact hpositive_right
06Separate the logical casesL24–24

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

  1. L24
    split
07Fix variables and assumptionsL25–25

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

  1. L25
    intro hb
08Establish hevenzeroL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul ne zero.

  1. L26
    have hevenzero : 2 * (m * n) = 0
  2. L27
    trans b
  3. L28
    symm
  4. L29
    exact hp_right_right_right_right_right_right
  5. L30
    exact hb
  6. L31
    apply mul_ne_zero
  7. L32
    intro htwo
  8. L33
    apply succ_ne_zero
  9. L34
    exact htwo
  10. L35
    intro hproduct
09Use earlier factsL36–40

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

  1. L36
    apply mul_ne_zero
  2. L37
    exact hpositive_left
  3. L38
    exact hp_left
  4. L39
    exact hproduct
  5. L40
    exact hevenzero
10Separate the logical casesL41–41

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

  1. L41
    split
11Fix variables and assumptionsL42–42

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

  1. L42
    intro hc
12Use earlier factsL43–46

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

  1. L43
    specialize pythagorean_hypotenuse_nonzero m
  2. L44
    specialize pythagorean_hypotenuse_nonzero n
  3. L45
    apply pythagorean_hypotenuse_nonzero
  4. L46
    exact hpositive_left
13Calculate and transport equalitiesL47–48

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L47
    trans c
  2. L48
    symm
14Use earlier factsL49–50

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

  1. L49
    exact hp_right_right_right_right_left
  2. L50
    exact hc
15Calculate and transport equalitiesL51–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L51
    rewrite hp_right_right_right_right_left
  2. L52
    rewrite hp_right_right_right_right_left
  3. L53
    rewrite hp_right_right_right_right_right_right
  4. L54
    rewrite hp_right_right_right_right_right_right
  5. L55
    rewrite hp_right_right_right_right_right_right
16Use earlier factsL56–62

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

  1. L56
    specialize pythagorean_primitive_euclidean_constructor m
  2. L57
    specialize pythagorean_primitive_euclidean_constructor n
  3. L58
    specialize pythagorean_primitive_euclidean_constructor a
  4. L59
    apply pythagorean_primitive_euclidean_constructor
  5. L60
    exact hp_right_right_right_right_right_left
  6. L61
    exact hp_right_right_left
  7. L62
    exact hp_right_right_right_left

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro m
  5. 0005intro n
  6. 0006intro hp
  7. 0007cases hp
  8. 0008cases hp_right
  9. 0009cases hp_right_right
  10. 0010cases hp_right_right_right
  11. 0011cases hp_right_right_right_right
  12. 0012cases hp_right_right_right_right_right
  13. 0013have hpositive : ~(m = 0) /\ ~(a = 0)
  14. 0014specialize pythagorean_ordered_gap_positive a
  15. 0015specialize pythagorean_ordered_gap_positive m
  16. 0016specialize pythagorean_ordered_gap_positive n
  17. 0017apply pythagorean_ordered_gap_positive
  18. 0018exact hp_left
  19. 0019exact hp_right_left
  20. 0020exact hp_right_right_right_right_right_left
  21. 0021cases hpositive
  22. 0022split
  23. 0023exact hpositive_right
  24. 0024split
  25. 0025intro hb
  26. 0026have hevenzero : 2 * (m * n) = 0
  27. 0027trans b
  28. 0028symm
  29. 0029exact hp_right_right_right_right_right_right
  30. 0030exact hb
  31. 0031apply mul_ne_zero
  32. 0032intro htwo
  33. 0033apply succ_ne_zero
  34. 0034exact htwo
  35. 0035intro hproduct
  36. 0036apply mul_ne_zero
  37. 0037exact hpositive_left
  38. 0038exact hp_left
  39. 0039exact hproduct
  40. 0040exact hevenzero
  41. 0041split
  42. 0042intro hc
  43. 0043specialize pythagorean_hypotenuse_nonzero m
  44. 0044specialize pythagorean_hypotenuse_nonzero n
  45. 0045apply pythagorean_hypotenuse_nonzero
  46. 0046exact hpositive_left
  47. 0047trans c
  48. 0048symm
  49. 0049exact hp_right_right_right_right_left
  50. 0050exact hc
  51. 0051rewrite hp_right_right_right_right_left
  52. 0052rewrite hp_right_right_right_right_left
  53. 0053rewrite hp_right_right_right_right_right_right
  54. 0054rewrite hp_right_right_right_right_right_right
  55. 0055rewrite hp_right_right_right_right_right_right
  56. 0056specialize pythagorean_primitive_euclidean_constructor m
  57. 0057specialize pythagorean_primitive_euclidean_constructor n
  58. 0058specialize pythagorean_primitive_euclidean_constructor a
  59. 0059apply pythagorean_primitive_euclidean_constructor
  60. 0060exact hp_right_right_right_right_right_left
  61. 0061exact hp_right_right_left
  62. 0062exact hp_right_right_right_left