PF0021

pythagorean_euclidean_parameters_positive_constructor

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 62 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

PF0020 pythagorean_ordered_gap_positive PF000T pythagorean_primitive_euclidean_constructor PF000A pythagorean_hypotenuse_nonzero mul_ne_zero Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

PF0022 pythagorean_positive_primitive_from_parameters

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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