PF001W · theorem body

pythagorean_half_factors_extract_parameters

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

Constructive coprime square-factor extraction recovers positive ordered coprime opposite-parity Euclid parameters and every coordinate 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. ∀ h. ∀ t. ¬a = 0 → ¬b = 0 → Odd(c) → b = 2 · h → c = a + 2 · t → (a + t) · t = h · h → Coprime(a + t,t) → ∃ x. ∃ y. EuclidParameters(a,b,c,x,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

ND0070 EuclidParameters PD0005 Coprime PD0010 Odd

In local proof propositions

none
Exact expanded first-order statement
forall a b c h t. ~(a = 0) -> ~(b = 0) -> (exists pp_odd_pi_extract_c. (c) = 2 * pp_odd_pi_extract_c + 1) -> b = 2 * h -> c = a + 2 * t -> (a + t) * t = h * h -> (forall pff_divisor_pi_extract_source. (exists pff_left_pi_extract_source. (a + t) = pff_divisor_pi_extract_source * pff_left_pi_extract_source) -> (exists pff_right_pi_extract_source. (t) = pff_divisor_pi_extract_source * pff_right_pi_extract_source) -> pff_divisor_pi_extract_source = 1) -> exists m n. ((~((n) = 0) /\ ((exists pi_gap_extract_result. pi_gap_extract_result + S (n) = (m)) /\ ((forall pff_divisor_pi_extract_result_coprime. (exists pff_left_pi_extract_result_coprime. (m) = pff_divisor_pi_extract_result_coprime * pff_left_pi_extract_result_coprime) -> (exists pff_right_pi_extract_result_coprime. (n) = pff_divisor_pi_extract_result_coprime * pff_right_pi_extract_result_coprime) -> pff_divisor_pi_extract_result_coprime = 1) /\ (((((exists pp_even_pi_extract_result_parity_first_even. (m) = 2 * pp_even_pi_extract_result_parity_first_even) /\ (exists pp_odd_pi_extract_result_parity_second_odd. (n) = 2 * pp_odd_pi_extract_result_parity_second_odd + 1)) \/ ((exists pp_odd_pi_extract_result_parity_first_odd. (m) = 2 * pp_odd_pi_extract_result_parity_first_odd + 1) /\ (exists pp_even_pi_extract_result_parity_second_even. (n) = 2 * pp_even_pi_extract_result_parity_second_even)))) /\ ((c) = (m) * (m) + (n) * (n) /\ ((m) * (m) = (n) * (n) + (a) /\ (b) = 2 * ((m) * (n)))))))))

Proof neighborhood

Direct theorem prerequisites

PF001E coprime_square_product_factors PF001R pythagorean_half_roots_coordinates PF001S pythagorean_half_roots_even_leg PF001O pythagorean_coprime_square_roots PF001U pythagorean_positive_even_leg_parameters_nonzero PF001T pythagorean_positive_gap_orders_parameters PF001Q pythagorean_odd_square_sum_opposite_roots

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

82 script commands · 27 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 (7)
coprime square product factorspythagorean half roots coordinatespythagorean half roots even legpythagorean coprime square rootspythagorean positive even leg parameters nonzeropythagorean positive gap orders parameterspythagorean odd square sum opposite roots
01Fix variables and assumptionsL1–10

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 h
  5. L5
    intro t
  6. L6
    intro ha
  7. L7
    intro hb
  8. L8
    intro hcodd
  9. L9
    intro hbeq
  10. L10
    intro hceq
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hproduct
  2. L12
    intro hcop
03Establish hrootsL13–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply coprime square product factors.

  1. L13
    have hroots : exists m n. a + t = m * m /\ t = n * n
  2. L14
    specialize coprime_square_product_factors (a + t)
  3. L15
    specialize coprime_square_product_factors t
  4. L16
    specialize coprime_square_product_factors h
  5. L17
    apply coprime_square_product_factors
  6. L18
    exact hcop
  7. L19
    exact hproduct
04Separate the logical casesL20–22

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

  1. L20
    cases hroots
  2. L21
    cases hroots_witness
  3. L22
    cases hroots_witness_witness
05Establish hcoordinatesL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean half roots coordinates.

  1. L23
    have hcoordinates : c = x * x + x1 * x1 /\ x * x = x1 * x1 + a
  2. L24
    specialize pythagorean_half_roots_coordinates a
  3. L25
    specialize pythagorean_half_roots_coordinates c
  4. L26
    specialize pythagorean_half_roots_coordinates t
  5. L27
    specialize pythagorean_half_roots_coordinates x
  6. L28
    specialize pythagorean_half_roots_coordinates x1
  7. L29
    apply pythagorean_half_roots_coordinates
  8. L30
    exact hceq
  9. L31
    exact hroots_witness_witness_left
  10. L32
    exact hroots_witness_witness_right
06Separate the logical casesL33–33

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

  1. L33
    cases hcoordinates
07Establish hlegL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean half roots even leg.

  1. L34
    have hleg : b = 2 * (x * x1)
  2. L35
    trans 2 * h
  3. L36
    exact hbeq
  4. L37
    specialize pythagorean_half_roots_even_leg a
  5. L38
    specialize pythagorean_half_roots_even_leg t
  6. L39
    specialize pythagorean_half_roots_even_leg h
  7. L40
    specialize pythagorean_half_roots_even_leg x
  8. L41
    specialize pythagorean_half_roots_even_leg x1
  9. L42
    apply pythagorean_half_roots_even_leg
  10. L43
    exact hproduct
08Use earlier factsL44–45

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

  1. L44
    exact hroots_witness_witness_left
  2. L45
    exact hroots_witness_witness_right
09Establish hpositiveL46–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean positive even leg parameters nonzero.

  1. L46
    have hpositive : ~(x = 0) /\ ~(x1 = 0)
  2. L47
    specialize pythagorean_positive_even_leg_parameters_nonzero b
  3. L48
    specialize pythagorean_positive_even_leg_parameters_nonzero x
  4. L49
    specialize pythagorean_positive_even_leg_parameters_nonzero x1
  5. L50
    apply pythagorean_positive_even_leg_parameters_nonzero
  6. L51
    exact hb
  7. L52
    exact hleg
10Separate the logical casesL53–53

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

  1. L53
    cases hpositive
11Construct an explicit witnessL54–55

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

  1. L54
    exists x
  2. L55
    exists x1
12Separate the logical casesL56–56

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

  1. L56
    split
13Use earlier factsL57–57

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

  1. L57
    exact hpositive_right
14Separate the logical casesL58–58

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

  1. L58
    split
15Use earlier factsL59–64

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

  1. L59
    specialize pythagorean_positive_gap_orders_parameters a
  2. L60
    specialize pythagorean_positive_gap_orders_parameters x
  3. L61
    specialize pythagorean_positive_gap_orders_parameters x1
  4. L62
    apply pythagorean_positive_gap_orders_parameters
  5. L63
    exact ha
  6. L64
    exact hcoordinates_right
16Separate the logical casesL65–65

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

  1. L65
    split
17Use earlier factsL66–68

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

  1. L66
    specialize pythagorean_coprime_square_roots x
  2. L67
    specialize pythagorean_coprime_square_roots x1
  3. L68
    apply pythagorean_coprime_square_roots
18Calculate and transport equalitiesL69–70

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

  1. L69
    rewrite <- hroots_witness_witness_left
  2. L70
    rewrite <- hroots_witness_witness_right
19Use earlier factsL71–71

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

  1. L71
    exact hcop
20Separate the logical casesL72–72

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

  1. L72
    split
21Use earlier factsL73–75

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

  1. L73
    specialize pythagorean_odd_square_sum_opposite_roots x
  2. L74
    specialize pythagorean_odd_square_sum_opposite_roots x1
  3. L75
    apply pythagorean_odd_square_sum_opposite_roots
22Calculate and transport equalitiesL76–76

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

  1. L76
    rewrite <- hcoordinates_left
23Use earlier factsL77–77

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

  1. L77
    exact hcodd
24Separate the logical casesL78–78

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

  1. L78
    split
25Use earlier factsL79–79

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

  1. L79
    exact hcoordinates_left
26Separate the logical casesL80–80

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

  1. L80
    split
27Use earlier factsL81–82

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

  1. L81
    exact hcoordinates_right
  2. L82
    exact hleg

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro h
  5. 0005intro t
  6. 0006intro ha
  7. 0007intro hb
  8. 0008intro hcodd
  9. 0009intro hbeq
  10. 0010intro hceq
  11. 0011intro hproduct
  12. 0012intro hcop
  13. 0013have hroots : exists m n. a + t = m * m /\ t = n * n
  14. 0014specialize coprime_square_product_factors (a + t)
  15. 0015specialize coprime_square_product_factors t
  16. 0016specialize coprime_square_product_factors h
  17. 0017apply coprime_square_product_factors
  18. 0018exact hcop
  19. 0019exact hproduct
  20. 0020cases hroots
  21. 0021cases hroots_witness
  22. 0022cases hroots_witness_witness
  23. 0023have hcoordinates : c = x * x + x1 * x1 /\ x * x = x1 * x1 + a
  24. 0024specialize pythagorean_half_roots_coordinates a
  25. 0025specialize pythagorean_half_roots_coordinates c
  26. 0026specialize pythagorean_half_roots_coordinates t
  27. 0027specialize pythagorean_half_roots_coordinates x
  28. 0028specialize pythagorean_half_roots_coordinates x1
  29. 0029apply pythagorean_half_roots_coordinates
  30. 0030exact hceq
  31. 0031exact hroots_witness_witness_left
  32. 0032exact hroots_witness_witness_right
  33. 0033cases hcoordinates
  34. 0034have hleg : b = 2 * (x * x1)
  35. 0035trans 2 * h
  36. 0036exact hbeq
  37. 0037specialize pythagorean_half_roots_even_leg a
  38. 0038specialize pythagorean_half_roots_even_leg t
  39. 0039specialize pythagorean_half_roots_even_leg h
  40. 0040specialize pythagorean_half_roots_even_leg x
  41. 0041specialize pythagorean_half_roots_even_leg x1
  42. 0042apply pythagorean_half_roots_even_leg
  43. 0043exact hproduct
  44. 0044exact hroots_witness_witness_left
  45. 0045exact hroots_witness_witness_right
  46. 0046have hpositive : ~(x = 0) /\ ~(x1 = 0)
  47. 0047specialize pythagorean_positive_even_leg_parameters_nonzero b
  48. 0048specialize pythagorean_positive_even_leg_parameters_nonzero x
  49. 0049specialize pythagorean_positive_even_leg_parameters_nonzero x1
  50. 0050apply pythagorean_positive_even_leg_parameters_nonzero
  51. 0051exact hb
  52. 0052exact hleg
  53. 0053cases hpositive
  54. 0054exists x
  55. 0055exists x1
  56. 0056split
  57. 0057exact hpositive_right
  58. 0058split
  59. 0059specialize pythagorean_positive_gap_orders_parameters a
  60. 0060specialize pythagorean_positive_gap_orders_parameters x
  61. 0061specialize pythagorean_positive_gap_orders_parameters x1
  62. 0062apply pythagorean_positive_gap_orders_parameters
  63. 0063exact ha
  64. 0064exact hcoordinates_right
  65. 0065split
  66. 0066specialize pythagorean_coprime_square_roots x
  67. 0067specialize pythagorean_coprime_square_roots x1
  68. 0068apply pythagorean_coprime_square_roots
  69. 0069rewrite <- hroots_witness_witness_left
  70. 0070rewrite <- hroots_witness_witness_right
  71. 0071exact hcop
  72. 0072split
  73. 0073specialize pythagorean_odd_square_sum_opposite_roots x
  74. 0074specialize pythagorean_odd_square_sum_opposite_roots x1
  75. 0075apply pythagorean_odd_square_sum_opposite_roots
  76. 0076rewrite <- hcoordinates_left
  77. 0077exact hcodd
  78. 0078split
  79. 0079exact hcoordinates_left
  80. 0080split
  81. 0081exact hcoordinates_right
  82. 0082exact hleg