Grace/Cumulus/Real/RootTwoRational.g17

Open in Workbench Download source

Imports

RationalEmbedding · RootTwo · NumberTheory.RootTwo

Declarations

Source

1-- The real square root of two is not rational2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.RootTwoRational8import RationalEmbedding9import RootTwo10import NumberTheory.RootTwo1112theorem sqrtTwo.square_scaled (m : Nat)13  shows (√2 * realNat(m)) * (√2 * realNat(m)) = (2:R) * (realNat(m) * realNat(m))14proof15  have one := realZero.lt_one16  have twoLe : (0:R) ≤ (2:R) by linarith17  have twoNonnegative := NonnegativeReal.of_le with *18  have square := sqrt.square with *19  have expand : (√2 * realNat(m)) * (√2 * realNat(m)) = (√2 * √2) * (realNat(m) * realNat(m)) by ring20  rw [expand, square]21  rfl2223-- (√2 · m)² is never the square of a natural number when m is positive.24theorem sqrtTwo.scaled_square_ne (d m : Nat)25  requires nonzero : m ≠ 026  shows (√2 * realNat(m)) * (√2 * realNat(m)) ≠ realNat(d) * realNat(d)27proof28  intro equal29  have scaled := sqrtTwo.square_scaled at m with *30  rw scaled at equal31  have left : realNat(2 * (m * m)) = (2:R) * (realNat(m) * realNat(m))32    rw [realNat.mul, realNat.mul, realNat.two]33    rfl34  have right : realNat(d * d) = realNat(d) * realNat(d)35    exact realNat.mul with *36  have natural : realNat(2 * (m * m)) = realNat(d * d) by rwa [left, right]37  have equalNaturals := realNat.injective with *38  have contradiction := rootTwo.irrational at d, m with *39  symm at equalNaturals40  exact contradiction with equalNaturals4142-- √2 is not the cut of any rational. A rational is (a − b)/m with m positive,43-- so √2 · m would be the difference of two naturals, and its square the square44-- of a natural.45theorem sqrtTwo.ne_rationalCut (q : Rational)46  shows √2 ≠ rationalCut(q)47proof48  intro equal49  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates at q with *50  have scaled := rationalCut.scaled at a, b, m with *51  rw [← qShape, ← equal] at scaled52  have one := realZero.lt_one53  have twoLe : (0:R) ≤ (2:R) by linarith54  have twoNonnegative := NonnegativeReal.of_le with *55  have shape := LessEqual.total at a, b with *56  cases shape with le | ge57  . obtain ⟨d, dNat, equation⟩ := le58    have expand : realNat(b) = (realNat(a):R) + (realNat(d):R)59      rw [← equation, realNat.add]60      rfl61    have squares : (√2 * realNat(m)) * (√2 * realNat(m)) = realNat(d) * realNat(d)62      rw [scaled, expand]63      ring64    exact sqrtTwo.scaled_square_ne with *, squares65  . obtain ⟨d, dNat, equation⟩ := ge66    have expand : realNat(a) = (realNat(b):R) + (realNat(d):R)67      rw [← equation, realNat.add]68      rfl69    have squares : (√2 * realNat(m)) * (√2 * realNat(m)) = realNat(d) * realNat(d)70      rw [scaled, expand]71      ring72    exact sqrtTwo.scaled_square_ne with *, squares73