Grace/Cumulus/NumberTheory/PerfectSquares.g17

Open in Workbench Download source

Imports

ModularMore

Declarations

Source

1-- Perfect squares and sums of two squares: squares are closed under2-- products, a square is 0 or 1 modulo 3 and modulo 4, an odd square is 13-- modulo 8, there is no square strictly between consecutive squares, and the4-- product of two sums of two squares is a sum of two squares5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.NumberTheory.PerfectSquares11import ModularMore1213predicate IsSquare (n : Nat) := ∃ k, Nat(k) ∧ n = k * k1415theorem IsSquare.intro (k : Nat)16  shows IsSquare(k * k)17proof18  witness k19  rfl2021theorem IsSquare.zero22  shows IsSquare(0)23proof24  witness 025  ring2627theorem IsSquare.one28  shows IsSquare(1)29proof30  witness 131  ring3233theorem IsSquare.pow_two (k : Nat)34  shows IsSquare(k ^ 2)35proof36  have square := pow.two at k37  rw square38  exact IsSquare.intro at k3940theorem IsSquare.pow_double (a k : Nat)41  shows IsSquare(a ^ (2 * k))42proof43  have double := pow.double_exponent at a, k44  rw double45  exact IsSquare.pow_two at a ^ k4647theorem IsSquare.mul (m n : Nat)48  requires first : IsSquare(m)49  requires second : IsSquare(n)50  shows IsSquare(m * n)51proof52  obtain ⟨a, aNat, aShape⟩ := first53  obtain ⟨b, bNat, bShape⟩ := second54  witness a * b55  rw [aShape, bShape]56  ring5758theorem IsSquare.mod_four (n : Nat)59  requires square : IsSquare(n)60  shows n % 4 = 0 ∨ n % 4 = 161proof62  obtain ⟨k, kNat, shape⟩ := square63  rw shape64  have four : 4 ≠ 0 by arith65  have reduce := mod.mul at 4, k, k with four66  rw reduce67  have alternatives := mod.four_cases at k68  rcases alternatives with zero | one | two | three69  . left70    rw zero71    compute72  . right73    rw one74    compute75  . left76    rw two77    compute78  . right79    rw three80    compute8182theorem IsSquare.mod_three (n : Nat)83  requires square : IsSquare(n)84  shows n % 3 = 0 ∨ n % 3 = 185proof86  obtain ⟨k, kNat, shape⟩ := square87  rw shape88  have three : 3 ≠ 0 by arith89  have reduce := mod.mul at 3, k, k with three90  rw reduce91  have alternatives := mod.three_cases at k92  rcases alternatives with zero | one | two93  . left94    rw zero95    compute96  . right97    rw one98    compute99  . right100    rw two101    compute102103theorem IsSquare.mod_three_ne_two (n : Nat)104  requires square : IsSquare(n)105  shows n % 3 ≠ 2106proof107  have alternatives := IsSquare.mod_three with square108  intro two109  rw two at alternatives110  cases alternatives with zero | one111  . arith112  . arith113114theorem IsSquare.mod_four_ne_two (n : Nat)115  requires square : IsSquare(n)116  shows n % 4 ≠ 2117proof118  have alternatives := IsSquare.mod_four with square119  intro two120  rw two at alternatives121  cases alternatives with zero | one122  . arith123  . arith124125theorem IsSquare.mod_four_ne_three (n : Nat)126  requires square : IsSquare(n)127  shows n % 4 ≠ 3128proof129  have alternatives := IsSquare.mod_four with square130  intro three131  rw three at alternatives132  cases alternatives with zero | one133  . arith134  . arith135136theorem Odd.square_mod_eight (k : Nat)137  requires odd : Odd(k)138  shows (k * k) % 8 = 1139proof140  obtain ⟨j, jNat, shape⟩ := Odd.iff_two_mul_add_one.forward with odd141  have evenProduct : Even(j * (j + 1))142    have parity := parity.exhaustive at j143    cases parity with even | oddJ144    . exact Even.mul_left at j, j + 1 with even145    . have succEven := Even.succ_of_odd at j with oddJ146      have one := add.right_one at j147      rw one148      exact Even.mul_right at j, succ(j) with succEven149  obtain ⟨m, mNat, mShape⟩ := Even.iff_two_mul.forward with evenProduct150  have expand : k * k = 8 * m + 1151    rw shape152    ring [mShape]153  rw expand154  have eight : 8 ≠ 0 by arith155  have reduce := mod.multiple_add at 8, 1, m with eight156  rw reduce157  compute158159theorem IsSquare.odd_mod_eight (n : Nat)160  requires square : IsSquare(n)161  requires odd : Odd(n)162  shows n % 8 = 1163proof164  obtain ⟨k, kNat, shape⟩ := square165  rw shape at odd166  have both := Odd.of_mul at k, k with odd167  rw shape168  exact Odd.square_mod_eight with both.left169170theorem IsSquare.even_iff (n : Nat)171  requires square : IsSquare(n)172  shows Even(n) ↔ ∃ k, Nat(k) ∧ Even(k) ∧ n = k * k173proof174  obtain ⟨k, kNat, shape⟩ := square175  constructor176  . intro even177    rw shape at even178    have characterization := Even.mul_self_iff at k179    have kEven := characterization.forward with even180    exact ⟨k, kNat, kEven, shape⟩181  . intro witnessed182    obtain ⟨j, jNat, jEven, jShape⟩ := witnessed183    rw jShape184    exact Even.mul_left at j, j with jEven185186-- Strictly increasing squares: a square below another has the smaller root.187theorem IsSquare.root_lt (k m : Nat)188  requires below : k * k < m * m189  shows k < m190proof191  by_contra notLess192  have above := LessEqual.of_not_Less with notLess193  have squares := LessEqual.mul at m, k, m, k with above, above194  have cycle := Less.transitive_LessEqual with below, squares195  exact Less.irreflexive at k * k with cycle196197theorem IsSquare.not_between (k n : Nat)198  requires lower : k * k < n199  requires upper : n < (k + 1) * (k + 1)200  shows ¬IsSquare(n)201proof202  intro square203  obtain ⟨m, mNat, shape⟩ := square204  rw shape at lower205  rw shape at upper206  have first := IsSquare.root_lt at k, m with lower207  have second := IsSquare.root_lt at m, k + 1 with upper208  arith209210theorem IsSquare.not_two211  shows ¬IsSquare(2)212proof213  have lower : 1 * 1 < 2 by arith214  have square : (1 + 1) * (1 + 1) = 2 * 2 by compute215  have upper : 2 < (1 + 1) * (1 + 1)216    rw square217    arith218  exact IsSquare.not_between at 1, 2 with lower, upper219220theorem IsSquare.not_three221  shows ¬IsSquare(3)222proof223  have lower : 1 * 1 < 3 by arith224  have square : (1 + 1) * (1 + 1) = 2 * 2 by compute225  have upper : 3 < (1 + 1) * (1 + 1)226    rw square227    arith228  exact IsSquare.not_between at 1, 3 with lower, upper229230theorem IsSquare.not_five231  shows ¬IsSquare(5)232proof233  have lower : 2 * 2 < 5 by arith234  have square : (2 + 1) * (2 + 1) = 3 * 3 by compute235  have upper : 5 < (2 + 1) * (2 + 1)236    rw square237    arith238  exact IsSquare.not_between at 2, 5 with lower, upper239240predicate SumOfTwoSquares (n : Nat) :=241  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ n = a * a + b * b242243theorem SumOfTwoSquares.intro (a b : Nat)244  shows SumOfTwoSquares(a * a + b * b)245proof246  refine ⟨a, assumption, b, assumption, _⟩247  rfl248249theorem SumOfTwoSquares.of_square (n : Nat)250  requires square : IsSquare(n)251  shows SumOfTwoSquares(n)252proof253  obtain ⟨k, kNat, shape⟩ := square254  have zero : k * k = k * k + 0 * 0 by ring255  rw [shape, zero]256  exact SumOfTwoSquares.intro at k, 0257258theorem SumOfTwoSquares.zero259  shows SumOfTwoSquares(0)260proof261  have square := IsSquare.zero262  exact SumOfTwoSquares.of_square with square263264theorem SumOfTwoSquares.one265  shows SumOfTwoSquares(1)266proof267  have square := IsSquare.one268  exact SumOfTwoSquares.of_square with square269270theorem SumOfTwoSquares.two271  shows SumOfTwoSquares(2)272proof273  have shape : 2 = 1 * 1 + 1 * 1 by compute274  rw shape275  exact SumOfTwoSquares.intro at 1, 1276277-- The Brahmagupta–Fibonacci identity, with the signed cross term replaced278-- by the distance between the two cross products.279theorem SumOfTwoSquares.product_identity (a b c d : Nat)280  shows281    (a * a + b * b) * (c * c + d * d) =282      (a * c + b * d) * (a * c + b * d) +283        natDist(a * d, b * c) * natDist(a * d, b * c)284proof285  have total := LessEqual.total at b * c, a * d286  cases total with below | above287  . obtain ⟨e, eNat, split⟩ := LessEqual.exists_add with below288    have characterization := natDist.eq_iff at a * d, b * c, e289    have distance : natDist(a * d, b * c) = e290      apply characterization.backward291      right292      exact split293    rw distance294    ring [split]295  . obtain ⟨e, eNat, split⟩ := LessEqual.exists_add with above296    have characterization := natDist.eq_iff at a * d, b * c, e297    have distance : natDist(a * d, b * c) = e298      apply characterization.backward299      left300      exact split301    rw distance302    ring [split]303304theorem SumOfTwoSquares.mul (m n : Nat)305  requires first : SumOfTwoSquares(m)306  requires second : SumOfTwoSquares(n)307  shows SumOfTwoSquares(m * n)308proof309  obtain ⟨a, aNat, b, bNat, mShape⟩ := first310  obtain ⟨c, cNat, d, dNat, nShape⟩ := second311  have identity := SumOfTwoSquares.product_identity at a, b, c, d312  rw [mShape, nShape, identity]313  exact SumOfTwoSquares.intro at a * c + b * d, natDist(a * d, b * c)314315theorem SumOfTwoSquares.mod_four (n : Nat)316  requires sum : SumOfTwoSquares(n)317  shows n % 4 ≠ 3318proof319  obtain ⟨a, aNat, b, bNat, shape⟩ := sum320  intro three321  rw shape at three322  have four : 4 ≠ 0 by arith323  have reduce := mod.add at 4, a * a, b * b with four324  rw reduce at three325  have squareA := IsSquare.intro at a326  have squareB := IsSquare.intro at b327  have leftCases := IsSquare.mod_four with squareA328  have rightCases := IsSquare.mod_four with squareB329  cases leftCases with leftZero | leftOne330  . rw leftZero at three331    cases rightCases with rightZero | rightOne332    . rw rightZero at three333      have value : (0 + 0) % 4 = 0 by compute334      rw value at three335      arith336    . rw rightOne at three337      have value : (0 + 1) % 4 = 1 by compute338      rw value at three339      arith340  . rw leftOne at three341    cases rightCases with rightZero | rightOne342    . rw rightZero at three343      have value : (1 + 0) % 4 = 1 by compute344      rw value at three345      arith346    . rw rightOne at three347      have value : (1 + 1) % 4 = 2 by compute348      rw value at three349      arith350