Grace/Cumulus/NumberTheory/PythagoreanTriples.g17

Open in Workbench Download source

Imports

CoprimeSquares

Declarations

Source

1-- Pythagorean triples: the parametrization (m² − n², 2mn, m² + n²) gives2-- every primitive triple with an even second leg, and every triple is a3-- multiple of a primitive one4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.PythagoreanTriples10import CoprimeSquares1112-- Positive naturals a, b, c with a² + b² = c².13predicate Pythagorean (a b c : Nat) := 0 < a ∧ 0 < b ∧ a ^ 2 + b ^ 2 = c ^ 21415-- A Pythagorean triple whose legs are coprime.16predicate PrimitivePythagorean (a b c : Nat) :=17  Pythagorean(a, b, c) ∧ gcd(a, b) = 11819-- Squaring is injective on the naturals.20theorem IsSquare.root_unique (x y : Nat)21  requires squares : x * x = y * y22  shows x = y23proof24  have order := Less.trichotomy at x, y with *25  rcases order with below | equal | above26  . exfalso27    have strict := Less.mul at x, y, x, y with below, below28    rw squares at strict29    exact Less.irreflexive at y * y with strict30  . exact equal31  . exfalso32    have strict := Less.mul at y, x, y, x with above, above33    rw squares at strict34    exact Less.irreflexive at y * y with strict3536theorem Odd.square_mod_four (k : Nat)37  requires odd : Odd(k)38  shows (k * k) % 4 = 139proof40  obtain ⟨j, jNat, shape⟩ := Odd.iff_two_mul_add_one.forward with odd41  have expand : k * k = 4 * (j * j + j) + 142    rw shape43    ring44  rw expand45  have four : 4 ≠ 0 by arith46  have reduce := mod.multiple_add at 4, 1, j * j + j with four47  rw reduce48  compute4950-- An odd divisor of 2t divides t.51theorem divides.of_double_odd (d t : Nat)52  requires odd : Odd(d)53  requires double : d ∣ 2 * t54  shows d ∣ t55proof56  obtain ⟨k, kNat, product⟩ := double57  have evenK : Even(k)58    have evenProduct : Even(d * k)59      rw product60      exact Even.two_mul at t61    have split := Even.of_mul at d, k with evenProduct62    cases split with evenD | evenK63    . exfalso64      exact Odd.not_even with odd, evenD65    . exact evenK66  obtain ⟨j, jNat, kShape⟩ := Even.iff_two_mul.forward with evenK67  witness j68  have scaled : 2 * (d * j) = 2 * t69    rw [← product, kShape]70    ring71  have two : 2 ≠ 0 by arith72  exact mul.left_cancel_positive at d * j, t, 2 with two, scaled7374-- With m² = n² + d, the difference d has the parity of m + n.75theorem Even.root_sum_iff (m n d : Nat)76  requires shape : m * m = n * n + d77  shows Even(m + n) ↔ Even(d)78proof79  have squareM := Even.mul_self_iff at m80  have squareN := Even.mul_self_iff at n81  have sumMN := Even.add_iff at m, n82  have sumND := Even.add_iff at n * n, d83  rw shape at squareM84  tauto8586-- The parametrization: for m > n > 0 the triple87-- (m² − n², 2mn, m² + n²) is Pythagorean.88theorem pythagorean.of_parameters (m n : Nat)89  requires positive : 0 < n90  requires below : n < m91  shows Pythagorean(m ^ 2 - n ^ 2, 2 * m * n, m ^ 2 + n ^ 2)92proof93  have squares := Less.mul at n, m, n, m with below, below94  have squaresLe : n * n ≤ m * m by arith95  obtain ⟨d, dNat, shape⟩ := LessEqual.exists_add at n * n, m * m96    with squaresLe97  have difference : m ^ 2 - n ^ 2 = d98    rw [pow.two, pow.two, shape]99    exact sub.add_left at d, n * n100  have dPositive : 0 < d by arith101  have productPositive : 0 < 2 * m * n102    have mNonzero : m ≠ 0 by arith103    have nNonzero : n ≠ 0 by arith104    have two : 2 ≠ 0 by arith105    have twoM := mul.nonzero at 2, m with two, mNonzero106    have all := mul.nonzero at 2 * m, n with twoM, nNonzero107    exact Less.positive_of_ne_zero at 2 * m * n with all108  unfold Pythagorean109  rw difference110  refine ⟨dPositive, productPositive, _⟩111  simp [pow.two]112  ring [shape]113114-- With m, n coprime and of opposite parity, the parametrized triple is115-- primitive: a common divisor e of m² − n² and 2mn is odd, hence divides116-- mn, and is coprime to m and to n, hence to mn.117theorem pythagorean.primitive_of_parameters (m n : Nat)118  requires positive : 0 < n119  requires below : n < m120  requires coprime : gcd(m, n) = 1121  requires parity : Odd(m + n)122  shows PrimitivePythagorean(m ^ 2 - n ^ 2, 2 * m * n, m ^ 2 + n ^ 2)123proof124  constructor125  . exact pythagorean.of_parameters at m, n with positive, below126  . have squares := Less.mul at n, m, n, m with below, below127    have squaresLe : n * n ≤ m * m by arith128    obtain ⟨d, dNat, shape⟩ := LessEqual.exists_add at n * n, m * m129      with squaresLe130    have difference : m ^ 2 - n ^ 2 = d131      rw [pow.two, pow.two, shape]132      exact sub.add_left at d, n * n133    rw difference134    have oddD : Odd(d)135      have parities := Even.root_sum_iff at m, n, d with shape136      have notEvenSum := Odd.not_even at m + n with parity137      have oddIff := Odd.iff_not_even at d138      apply oddIff.backward139      tauto140    have every := gcd.eq_one_iff at d, 2 * m * n141    apply every.backward142    intros e eNat ed eProduct143    have oddE : Odd(e)144      obtain ⟨k, kNat, product⟩ := ed145      rw ← product at oddD146      have both := Odd.of_mul at e, k with oddD147      exact both.left148    have regroup : 2 * m * n = 2 * (m * n) by ring149    rw regroup at eProduct150    have eDividesMN := divides.of_double_odd at e, m * n with oddE, eProduct151    have coprimeEM : gcd(e, m) = 1152      have everyM := gcd.eq_one_iff at e, m153      apply everyM.backward154      intros f fNat fe fm155      have fd := divides.transitive at f, e, d with fe, ed156      have fmm := divides.mul_self at f, m with fm157      have fnn : f ∣ n * n158        have cancel := sub.add_right at n * n, d159        rw [← cancel, ← shape]160        exact divides.sub at f, m * m, d with fmm, fd161      have coprimeFN := coprime.of_divides_left at m, n, f with coprime, fm162      have coprimeFNN := coprime.pow_right at f, n, 2 with coprimeFN163      rw pow.two at coprimeFNN164      have fSelf := divides.reflexive at f165      exact coprime.divisor_one at f, n * n, f with coprimeFNN, fSelf, fnn166    have coprimeEN : gcd(e, n) = 1167      have everyN := gcd.eq_one_iff at e, n168      apply everyN.backward169      intros f fNat fe fn170      have fd := divides.transitive at f, e, d with fe, ed171      have fnn := divides.mul_self at f, n with fn172      have fmm : f ∣ m * m173        rw shape174        exact divides.add at f, n * n, d with fnn, fd175      have coprimeNM := coprime.symmetric at m, n with coprime176      have coprimeFM := coprime.of_divides_left at n, m, f with coprimeNM, fn177      have coprimeFMM := coprime.pow_right at f, m, 2 with coprimeFM178      rw pow.two at coprimeFMM179      have fSelf := divides.reflexive at f180      exact coprime.divisor_one at f, m * m, f with coprimeFMM, fSelf, fmm181    have coprimeME := coprime.symmetric at e, m with coprimeEM182    have coprimeNE := coprime.symmetric at e, n with coprimeEN183    have coprimeMNE := coprime.mul_of_coprime at m, n, e184      with coprimeME, coprimeNE185    have coprimeEMN := coprime.symmetric at m * n, e with coprimeMNE186    have eSelf := divides.reflexive at e187    exact coprime.divisor_one at e, m * n, e with coprimeEMN, eSelf, eDividesMN188189-- In a primitive triple exactly one leg is even: two even legs share the190-- factor 2, and two odd legs give c² ≡ 2 modulo 4.191theorem pythagorean.one_even (a b c : Nat)192  requires primitive : PrimitivePythagorean(a, b, c)193  shows Odd(a + b)194proof195  obtain ⟨triple, coprime⟩ := primitive196  obtain ⟨positiveA, positiveB, equation⟩ := triple197  simp [pow.two] at equation198  have notBothEven : ¬(Even(a) ∧ Even(b))199    intro both200    have twoIffA := divides.two_iff_even at a201    have twoIffB := divides.two_iff_even at b202    have twoA := twoIffA.backward with both.left203    have twoB := twoIffB.backward with both.right204    have two := coprime.divisor_one at a, b, 2 with coprime, twoA, twoB205    arith206  have notBothOdd : ¬(Odd(a) ∧ Odd(b))207    intro both208    have modA := Odd.square_mod_four at a with both.left209    have modB := Odd.square_mod_four at b with both.right210    have four : 4 ≠ 0 by arith211    have reduce := mod.add at 4, a * a, b * b with four212    rw [modA, modB, equation] at reduce213    have value : (1 + 1) % 4 = 2 by compute214    rw value at reduce215    have square := IsSquare.intro at c216    have notTwo := IsSquare.mod_four_ne_two at c * c with square217    exact notTwo with reduce218  have evenIffA := Even.iff_not_odd at a219  have evenIffB := Even.iff_not_odd at b220  have sum := Even.add_iff at a, b221  have oddIff := Odd.iff_not_even at a + b222  apply oddIff.backward223  tauto224225-- Every primitive triple with b even comes from the parametrization: with226-- c = a + 2u and b = 2w, the equation gives w² = u(a + u) with u and a + u227-- coprime, so u = n² and a + u = m².228theorem pythagorean.primitive_form (a b c : Nat)229  requires primitive : PrimitivePythagorean(a, b, c)230  requires even : Even(b)231  shows ∃ m, Nat(m) ∧ ∃ n, Nat(n) ∧232    0 < n ∧ n < m ∧ gcd(m, n) = 1 ∧ Odd(m + n) ∧233    a = m ^ 2 - n ^ 2 ∧ b = 2 * m * n ∧ c = m ^ 2 + n ^ 2234proof235  have parity := pythagorean.one_even at a, b, c with primitive236  obtain ⟨triple, coprime⟩ := primitive237  obtain ⟨positiveA, positiveB, equation⟩ := triple238  simp [pow.two] at equation239  have oddA : Odd(a)240    have swapped : Odd(b + a)241      have commute : b + a = a + b by ring242      rw commute243      exact parity244    exact Odd.of_add_odd_even at b, a with swapped, even245  have oddC : Odd(c)246    have squareA := Odd.mul_self_iff at a247    have squareB := Even.mul_self_iff at b248    have oddSquareA := squareA.backward with oddA249    have evenSquareB := squareB.backward with even250    have oddSum := Odd.add_even at a * a, b * b with oddSquareA, evenSquareB251    rw equation at oddSum252    have squareC := Odd.mul_self_iff at c253    exact squareC.forward with oddSum254  have aBelowC : a < c255    have bNonzero : b ≠ 0 by arith256    have bbNonzero := mul.nonzero at b, b with bNonzero, bNonzero257    have bbPositive := Less.positive_of_ne_zero at b * b with bbNonzero258    have squares : a * a < c * c by arith259    exact IsSquare.root_lt at a, c with squares260  have aLeC : a ≤ c by arith261  obtain ⟨t, tNat, cShape⟩ := LessEqual.exists_add at a, c with aLeC262  have evenT : Even(t)263    rw cShape at oddC264    exact Even.of_add_odd_odd at a, t with oddC, oddA265  obtain ⟨u, uNat, tShape⟩ := Even.iff_two_mul.forward with evenT266  obtain ⟨w, wNat, bShape⟩ := Even.iff_two_mul.forward with even267  have key : u * (a + u) = w * w268    have expanded : 4 * (u * (a + u)) = 4 * (w * w)269      rw [bShape, cShape, tShape] at equation270      have leftSide : a * a + 2 * w * (2 * w) = a * a + 4 * (w * w) by ring271      have rightSide : (a + 2 * u) * (a + 2 * u) = a * a + 4 * (u * (a + u))272        ring273      rw [leftSide, rightSide] at equation274      have cancel := add.left_cancel at 4 * (w * w), 4 * (u * (a + u)), a * a275      have swapped := cancel with equation276      symm277      exact swapped278    have four : 4 ≠ 0 by arith279    exact mul.left_cancel_positive at u * (a + u), w * w, 4 with four, expanded280  have uPositive : 0 < u by arith281  have coprimeUV : gcd(u, a + u) = 1282    have every := gcd.eq_one_iff at u, a + u283    apply every.backward284    intros d dNat du dv285    have da := divides.sub at d, a + u, u with dv, du286    have cancel := sub.add_right at a, u287    rw cancel at da288    have dSquares := divides.mul_mono at d, u, d, a + u with du, dv289    rw key at dSquares290    have dw := divides.of_mul_self at d, w with dSquares291    have db : d ∣ b292      rw bShape293      exact divides.multiply_left at d, w, 2 with *294    exact coprime.divisor_one at a, b, d with coprime, da, db295  obtain ⟨squareU, squareV⟩ := IsSquare.of_coprime_mul at u, a + u, w296    with coprimeUV, key297  obtain ⟨n, nNat, uShape⟩ := squareU298  obtain ⟨m, mNat, vShape⟩ := squareV299  have nPositive : 0 < n300    have nNonzero : n ≠ 0301      intro nZero302      rw nZero at uShape303      have zero : 0 * 0 = 0 by compute304      rw zero at uShape305      arith306    exact Less.positive_of_ne_zero at n with nNonzero307  have nBelowM : n < m308    have squares : n * n < m * m309      rw [← uShape, ← vShape]310      arith311    exact IsSquare.root_lt at n, m with squares312  have coprimeMN : gcd(m, n) = 1313    have coprimeVU := coprime.symmetric at u, a + u with coprimeUV314    rw [vShape, uShape] at coprimeVU315    have coprimeMNN := coprime.of_mul_left at m, m, n * n with coprimeVU316    have coprimeNNM := coprime.symmetric at m, n * n with coprimeMNN317    have coprimeNM := coprime.of_mul_left at n, n, m with coprimeNNM318    exact coprime.symmetric at n, m with coprimeNM319  have parityMN : Odd(m + n)320    have shape : m * m = n * n + a321      rw [← vShape, ← uShape]322      ring323    have parities := Even.root_sum_iff at m, n, a with shape324    have notEvenA := Odd.not_even at a with oddA325    have oddIff := Odd.iff_not_even at m + n326    apply oddIff.backward327    tauto328  have aForm : a = m ^ 2 - n ^ 2329    rw [pow.two, pow.two, ← vShape, ← uShape]330    symm331    exact sub.add_right at a, u332  have wForm : w = m * n333    have squares : w * w = m * n * (m * n)334      rw [← key, vShape, uShape]335      ring336    exact IsSquare.root_unique at w, m * n with squares337  have bForm : b = 2 * m * n338    rw [bShape, wForm]339    ring340  have cForm : c = m ^ 2 + n ^ 2341    rw [pow.two, pow.two, ← vShape, ← uShape, cShape, tShape]342    ring343  exact ⟨m, mNat, n, nNat, nPositive, nBelowM, coprimeMN, parityMN, aForm,344    bForm, cForm⟩345346-- Every Pythagorean triple is gcd(a, b) times a primitive one.347theorem pythagorean.form (a b c : Nat)348  requires triple : Pythagorean(a, b, c)349  shows ∃ x, Nat(x) ∧ ∃ y, Nat(y) ∧ ∃ z, Nat(z) ∧350    PrimitivePythagorean(x, y, z) ∧351    a = gcd(a, b) * x ∧ b = gcd(a, b) * y ∧ c = gcd(a, b) * z352proof353  obtain ⟨positiveA, positiveB, equation⟩ := triple354  simp [pow.two] at equation355  have aNonzero : a ≠ 0 by arith356  have gcdNonzero := gcd.nonzero at a, b with aNonzero357  obtain ⟨x, xNat, aShape⟩ := gcd.divides_left at a, b358  obtain ⟨y, yNat, bShape⟩ := gcd.divides_right at a, b359  have cofactors := gcd.cofactor_coprime at a, b, x, y360    with gcdNonzero, aShape, bShape361  have squareDividesC : gcd(a, b) * gcd(a, b) ∣ c * c362    have dividesA := gcd.divides_left at a, b363    have dividesB := gcd.divides_right at a, b364    have left := divides.mul_mono at gcd(a, b), a, gcd(a, b), a365      with dividesA, dividesA366    have right := divides.mul_mono at gcd(a, b), b, gcd(a, b), b367      with dividesB, dividesB368    rw ← equation369    exact divides.add at gcd(a, b) * gcd(a, b), a * a, b * b with left, right370  have dividesC := divides.of_mul_self at gcd(a, b), c with squareDividesC371  obtain ⟨z, zNat, cShape⟩ := dividesC372  have reduced : x * x + y * y = z * z373    have scaled : gcd(a, b) * gcd(a, b) * (x * x + y * y) =374        gcd(a, b) * gcd(a, b) * (z * z)375      have leftSide : gcd(a, b) * gcd(a, b) * (x * x + y * y) = a * a + b * b376        ring [aShape, bShape]377      have rightSide : gcd(a, b) * gcd(a, b) * (z * z) = c * c by ring [cShape]378      rw [leftSide, rightSide]379      exact equation380    have squareNonzero := mul.nonzero at gcd(a, b), gcd(a, b)381      with gcdNonzero, gcdNonzero382    exact mul.left_cancel_positive at x * x + y * y, z * z,383      gcd(a, b) * gcd(a, b) with squareNonzero, scaled384  have positiveX : 0 < x385    have nonzero : x ≠ 0386      intro zero387      rw zero at aShape388      have value : gcd(a, b) * 0 = 0 by ring389      rw value at aShape390      arith391    exact Less.positive_of_ne_zero at x with nonzero392  have positiveY : 0 < y393    have nonzero : y ≠ 0394      intro zero395      rw zero at bShape396      have value : gcd(a, b) * 0 = 0 by ring397      rw value at bShape398      arith399    exact Less.positive_of_ne_zero at y with nonzero400  have primitive : PrimitivePythagorean(x, y, z)401    constructor402    . refine ⟨positiveX, positiveY, _⟩403      rw [pow.two, pow.two, pow.two]404      exact reduced405    . exact cofactors406  refine ⟨x, xNat, y, yNat, z, zNat, primitive, _, _, _⟩407  . symm408    exact aShape409  . symm410    exact bShape411  . symm412    exact cShape413