Grace/Cumulus/Real/RootTwo.g17

Open in Workbench Download source

Imports

Sqrt · Natural · NumberTheory.RootTwo

Declarations

Source

1-- The real square root of two is not a quotient of natural numbers2-- 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.RootTwo8import Sqrt9import Natural10import NumberTheory.RootTwo1112theorem realNat.nonnegative (n : Nat)13  shows (0:R) ≤ realNat(n)14proof15  induction n16  | zero =>17    rw realNat.zero18    linarith19  | succ(k) using ih =>20    rw realNat.succ21    have one := realZero.lt_one22    linarith2324theorem realNat.lt_of_lt (m n : Nat)25  requires less : m < n26  shows realNat(m) < realNat(n)27proof28  obtain ⟨k, kNat, equation⟩ := less29  rw [← equation, realNat.add, realNat.succ]30  have nonnegativeK := realNat.nonnegative at k with *31  have one := realZero.lt_one32  linarith3334theorem realNat.injective (m n : Nat)35  requires equal : realNat(m) = realNat(n)36  shows m = n37proof38  have shape := Less.trichotomy at m, n with *39  rcases shape with less | same | greater40  . exfalso41    have strict := realNat.lt_of_lt with *42    rw equal at strict43    exact realLess.not_self with *, strict44  . exact same45  . exfalso46    have strict := realNat.lt_of_lt with *47    rw equal at strict48    exact realLess.not_self with *, strict4950theorem realNat.nonzero (n : Nat)51  requires nonzero : n ≠ 052  shows realNat(n) ≠ (0:R)53proof54  intro zero55  rw ← realNat.zero at zero56  have equal := realNat.injective at n, 0 with *57  exact nonzero with equal5859theorem realNat.two60  shows realNat(2) = (2:R)61proof62  rw [realNat.succ, realNat.one]63  ring6465-- The real number √2 is not p/q for any naturals p and q. Since √2 is66-- positive, that rules out every rational.67theorem sqrtTwo.ne_quotient (p q : Nat)68  requires positive : q ≠ 069  shows √2 ≠ realNat(p) / realNat(q)70proof71  intro equation72  have qNonzero := realNat.nonzero with *73  have one := realZero.lt_one74  have twoLe : (0:R) ≤ (2:R) by linarith75  have twoNonnegative := NonnegativeReal.of_le with *76  have square := sqrt.square with *77  have scaled : √(2:R) * realNat(q) = realNat(p)78    rw equation79    exact realDiv.mul_right with *80  have squares : (√(2:R) * realNat(q)) * (√(2:R) * realNat(q)) = realNat(p) * realNat(p)81    rw scaled82    rfl83  have expand : (√(2:R) * realNat(q)) * (√(2:R) * realNat(q)) = (√(2:R) * √(2:R)) * (realNat(q) * realNat(q))84    ring85  rw [expand, square] at squares86  have left : realNat(2 * (q * q)) = (2:R) * (realNat(q) * realNat(q))87    rw [realNat.mul, realNat.mul, realNat.two]88    rfl89  have right : realNat(p * p) = realNat(p) * realNat(p)90    exact realNat.mul with *91  have natural : realNat(2 * (q * q)) = realNat(p * p) by rwa [left, right]92  have equalNaturals := realNat.injective with *93  have contradiction := rootTwo.irrational at p, q with *94  symm at equalNaturals95  exact contradiction with equalNaturals96