PF001V · theorem body

pythagorean_odd_even_half_factors

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

Every positive-even-leg primitive triangle constructs both coprime half-factors and their actual square-product equation.

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. PrimitivePythagorean(a,b,c) → ¬b = 0 → Odd(a) → Even(b) → ∃ x. ∃ y. b = 2 · x ∧ (c = a + 2 · y ∧ ((a + y) · y = x · x ∧ Coprime(a + y,y)))

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

CF0013 PrimitivePythagorean PD0005 Coprime PD0009 Even PD0010 Odd

In local proof propositions

PD0001 Le PD0005 Coprime PD0010 Odd
Exact expanded first-order statement
forall a b c. ((((a) * (a) + (b) * (b) = (c) * (c)) /\ (forall pff_divisor_pi_source. (exists pff_left_pi_source. (a) = pff_divisor_pi_source * pff_left_pi_source) -> (exists pff_right_pi_source. (b) = pff_divisor_pi_source * pff_right_pi_source) -> pff_divisor_pi_source = 1))) -> ~(b = 0) -> (exists pp_odd_pi_half_a. (a) = 2 * pp_odd_pi_half_a + 1) -> (exists pp_even_pi_half_b. (b) = 2 * pp_even_pi_half_b) -> exists h t. (b = 2 * h /\ (c = a + 2 * t /\ ((a + t) * t = h * h /\ (forall pff_divisor_pi_half_coprime. (exists pff_left_pi_half_coprime. (a + t) = pff_divisor_pi_half_coprime * pff_left_pi_half_coprime) -> (exists pff_right_pi_half_coprime. (t) = pff_divisor_pi_half_coprime * pff_right_pi_half_coprime) -> pff_divisor_pi_half_coprime = 1))))

Proof neighborhood

Direct theorem prerequisites

PF000W pythagorean_primitive_hypotenuse_coprime_first_leg PF0016 pythagorean_primitive_hypotenuse_odd PF001I pythagorean_leg_strictly_below_hypotenuse lt_to_le · Stable closed PF001J pythagorean_odd_ordered_difference_even PF001M pythagorean_half_product_is_square PF001N pythagorean_half_factors_coprime

Direct theorem dependents

PF001X pythagorean_primitive_odd_even_inverse

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

58 script commands · 18 reading checkpoints · 4 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 (6)
pythagorean primitive hypotenuse coprime first legpythagorean primitive hypotenuse oddpythagorean leg strictly below hypotenusepythagorean odd ordered difference evenpythagorean half product is squarepythagorean half factors coprime
01Fix variables and assumptionsL1–7

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
  5. L5
    intro hb
  6. L6
    intro haodd
  7. L7
    intro hbeven
02Establish hcopL8–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean primitive hypotenuse coprime first leg.

  1. L8
  2. L9
    specialize pythagorean_primitive_hypotenuse_coprime_first_leg a
  3. L10
    specialize pythagorean_primitive_hypotenuse_coprime_first_leg b
  4. L11
    specialize pythagorean_primitive_hypotenuse_coprime_first_leg c
  5. L12
    apply pythagorean_primitive_hypotenuse_coprime_first_leg
  6. L13
    exact hp
03Establish hcoddL14–19

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

  1. L14
  2. L15
    specialize pythagorean_primitive_hypotenuse_odd a
  3. L16
    specialize pythagorean_primitive_hypotenuse_odd b
  4. L17
    specialize pythagorean_primitive_hypotenuse_odd c
  5. L18
    apply pythagorean_primitive_hypotenuse_odd
  6. L19
    exact hp
04Establish hboundL20–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.

  1. L20
    have hbound : Le(a,c)Definitions: Le(a,c)Original native command in the exact edition
  2. L21
    apply lt_to_le
  3. L22
    specialize pythagorean_leg_strictly_below_hypotenuse a
  4. L23
    specialize pythagorean_leg_strictly_below_hypotenuse b
  5. L24
    specialize pythagorean_leg_strictly_below_hypotenuse c
  6. L25
    apply pythagorean_leg_strictly_below_hypotenuse
05Separate the logical casesL26–26

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

  1. L26
    cases hp
06Use earlier factsL27–28

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

  1. L27
    exact hp_left
  2. L28
    exact hb
07Establish hgapL29–33

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

  1. L29
    have hgap : exists t. c = a + 2 * t
  2. L30
    apply pythagorean_odd_ordered_difference_even
  3. L31
    exact hbound
  4. L32
    exact haodd
  5. L33
    exact hcodd
08Separate the logical casesL34–35

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

  1. L34
    cases hgap
  2. L35
    cases hbeven
09Construct an explicit witnessL36–37

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

  1. L36
    exists x1
  2. L37
    exists x
10Separate the logical casesL38–38

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

  1. L38
    split
11Use earlier factsL39–39

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

  1. L39
    exact hbeven_witness
12Separate the logical casesL40–40

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

  1. L40
    split
13Use earlier factsL41–41

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

  1. L41
    exact hgap_witness
14Separate the logical casesL42–42

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

  1. L42
    split
15Use earlier factsL43–47

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

  1. L43
    specialize pythagorean_half_product_is_square a
  2. L44
    specialize pythagorean_half_product_is_square c
  3. L45
    specialize pythagorean_half_product_is_square x1
  4. L46
    specialize pythagorean_half_product_is_square x
  5. L47
    apply pythagorean_half_product_is_square
16Calculate and transport equalitiesL48–49

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

  1. L48
    rewrite <- hbeven_witness
  2. L49
    rewrite <- hbeven_witness
17Separate the logical casesL50–50

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

  1. L50
    cases hp
18Use earlier factsL51–58

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

  1. L51
    exact hp_left
  2. L52
    exact hgap_witness
  3. L53
    specialize pythagorean_half_factors_coprime a
  4. L54
    specialize pythagorean_half_factors_coprime c
  5. L55
    specialize pythagorean_half_factors_coprime x
  6. L56
    apply pythagorean_half_factors_coprime
  7. L57
    exact hcop
  8. L58
    exact hgap_witness

Library-wide reading audit

Original defined command ledger · 58 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hp
  5. 0005intro hb
  6. 0006intro haodd
  7. 0007intro hbeven
  8. 0008have hcop : Coprime(a,c)
    Exact native replay linehave hcop : forall pff_divisor_pi_half_pair. (exists pff_left_pi_half_pair. (a) = pff_divisor_pi_half_pair * pff_left_pi_half_pair) -> (exists pff_right_pi_half_pair. (c) = pff_divisor_pi_half_pair * pff_right_pi_half_pair) -> pff_divisor_pi_half_pair = 1
  9. 0009specialize pythagorean_primitive_hypotenuse_coprime_first_leg a
  10. 0010specialize pythagorean_primitive_hypotenuse_coprime_first_leg b
  11. 0011specialize pythagorean_primitive_hypotenuse_coprime_first_leg c
  12. 0012apply pythagorean_primitive_hypotenuse_coprime_first_leg
  13. 0013exact hp
  14. 0014have hcodd : Odd(c)
    Exact native replay linehave hcodd : exists pp_odd_pi_half_hypotenuse. (c) = 2 * pp_odd_pi_half_hypotenuse + 1
  15. 0015specialize pythagorean_primitive_hypotenuse_odd a
  16. 0016specialize pythagorean_primitive_hypotenuse_odd b
  17. 0017specialize pythagorean_primitive_hypotenuse_odd c
  18. 0018apply pythagorean_primitive_hypotenuse_odd
  19. 0019exact hp
  20. 0020have hbound : Le(a,c)
    Exact native replay linehave hbound : exists gap. gap + a = c
  21. 0021apply lt_to_le
  22. 0022specialize pythagorean_leg_strictly_below_hypotenuse a
  23. 0023specialize pythagorean_leg_strictly_below_hypotenuse b
  24. 0024specialize pythagorean_leg_strictly_below_hypotenuse c
  25. 0025apply pythagorean_leg_strictly_below_hypotenuse
  26. 0026cases hp
  27. 0027exact hp_left
  28. 0028exact hb
  29. 0029have hgap : exists t. c = a + 2 * t
  30. 0030apply pythagorean_odd_ordered_difference_even
  31. 0031exact hbound
  32. 0032exact haodd
  33. 0033exact hcodd
  34. 0034cases hgap
  35. 0035cases hbeven
  36. 0036exists x1
  37. 0037exists x
  38. 0038split
  39. 0039exact hbeven_witness
  40. 0040split
  41. 0041exact hgap_witness
  42. 0042split
  43. 0043specialize pythagorean_half_product_is_square a
  44. 0044specialize pythagorean_half_product_is_square c
  45. 0045specialize pythagorean_half_product_is_square x1
  46. 0046specialize pythagorean_half_product_is_square x
  47. 0047apply pythagorean_half_product_is_square
  48. 0048rewrite <- hbeven_witness
  49. 0049rewrite <- hbeven_witness
  50. 0050cases hp
  51. 0051exact hp_left
  52. 0052exact hgap_witness
  53. 0053specialize pythagorean_half_factors_coprime a
  54. 0054specialize pythagorean_half_factors_coprime c
  55. 0055specialize pythagorean_half_factors_coprime x
  56. 0056apply pythagorean_half_factors_coprime
  57. 0057exact hcop
  58. 0058exact hgap_witness