Grace/Cumulus/NumberTheory/RootTwo.g17

Open in Workbench Download source

Imports

Nat.Parity · Nat.Least

Declarations

Source

1-- The square root of two is irrational2-- 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.NumberTheory.RootTwo8import Nat.Parity9import Nat.Least1011-- The square of an odd number is odd.12theorem Odd.square (n : Set)13  requires odd : Odd(n)14  shows Odd(n * n)15proof16  obtain ⟨k, kMember, equation⟩ := odd17  have kNat := nat.omega.backward with kMember18  have m : Nat(add(add(mul(k, k), mul(k, k)), add(k, k))) by typecheck19  witness add(add(mul(k, k), mul(k, k)), add(k, k))20  constructor21  . exact nat.omega.forward at add(add(mul(k, k), mul(k, k)), add(k, k)) with m22  . rw equation23    ring2425-- A number whose square is even is even.26theorem Even.of_square (n : Nat)27  requires even : Even(n * n)28  shows Even(n)29proof30  have shape := parity.exhaustive with *31  cases shape with evenN | oddN32  . exact evenN33  . exfalso34    have oddSquare := Odd.square with oddN35    exact Odd.not_even with *, even3637-- The naturals p with p² = 2q² for some positive q.38def rootTwoNumerators : Set :=39  { p ∈ ℕ | ∃ q ∈ ℕ, q ≠ 0 ∧ p * p = 2 * (q * q) }4041theorem rootTwoNumerators.subset_naturals42  shows rootTwoNumerators ⊆ ℕ43proof44  intros p member45  obtain ⟨natural, rest⟩ := rootTwoNumerators.membership.forward with member46  exact natural4748-- From p² = 2q² with q positive, p is even, p = 2j, and then q² = 2j² with49-- j positive and q < p. So q is a smaller member of the same set.50theorem rootTwoNumerators.descent (p q : Nat)51  requires positive : q ≠ 052  requires equation : p * p = 2 * (q * q)53  shows q ∈ rootTwoNumerators ∧ q < p54proof55  have evenSquare : Even(p * p)56    witness q * q57    constructor58    . have qq : Nat(q * q)59        typecheck60      exact nat.omega.forward with qq61    . rw equation62      exact mul.two_left with *63  have evenP := Even.of_square with *64  obtain ⟨j, jMember, pShape⟩ := evenP65  have jNat := nat.omega.backward with jMember66  have halved : q * q = 2 * (j * j)67    have doubled : 2 * (q * q) = 2 * (2 * (j * j))68      rw [← equation, pShape]69      simp [mul.two_left]70      ring71    have twoNonzero : 2 ≠ 072      intro bad73      have positiveTwo : 0 < 2 by arith74      rw bad at positiveTwo75      exact Less.irreflexive with *, positiveTwo76    exact mul.left_cancel_positive with *77  have jPositive : j ≠ 078    intro jZero79    rw jZero at halved80    have qq : q * q = 081      rw halved82      compute83    have split := mul.eq_zero with *, qq84    cases split with left | right85    . exact positive with left86    . exact positive with right87  have smaller : q < p88    have shape := Less.trichotomy at q, p with *89    rcases shape with less | equal | greater90    . exact less91    . exfalso92      rw [equal, pShape] at halved93      have two := mul.two_left at j * j with *94      rw two at halved95      have expand : (j + j) * (j + j) = (j * j + j * j) + (j * j + j * j) by ring96      rw expand at halved97      have upper : j * j ≤ 0 by arith98      have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at j * j with *99      have jj := LessEqual.antisymmetric at j * j, 0 with *100      have split := mul.eq_zero with *, jj101      cases split with first | second102      . exact jPositive with first103      . exact jPositive with second104    . exfalso105      have le := Less.implies_LessEqual with *106      have first := LessEqual.mul_left at p, q, p with *107      have second := LessEqual.mul_left at p, q, q with *108      have commuted := mul.commutative at q, p with *109      have two := mul.two_left at q * q with *110      rw two at equation111      have upper : q * q ≤ 0 by arith112      have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at q * q with *113      have zero := LessEqual.antisymmetric at q * q, 0 with *114      have split := mul.eq_zero with *, zero115      cases split with left | right116      . exact positive with left117      . exact positive with right118  constructor119  . apply rootTwoNumerators.membership.backward at q120    constructor121    . exact nat.omega.forward at q with assumption122    . witness j123      refine ⟨jMember, jPositive, halved⟩124  . exact smaller125126-- No natural p and positive q satisfy p² = 2q²: the least such p would give127-- a smaller one.128theorem rootTwo.irrational (p q : Nat)129  requires positive : q ≠ 0130  shows p * p ≠ 2 * (q * q)131proof132  intro equation133  have member : p ∈ rootTwoNumerators134    apply rootTwoNumerators.membership.backward135    constructor136    . exact nat.omega.forward at p with assumption137    . witness q138      have qMember := nat.omega.forward at q with assumption139      refine ⟨qMember, positive, equation⟩140  have inhabited : Nonempty(rootTwoNumerators) := ⟨p, member⟩141  have naturals := rootTwoNumerators.subset_naturals142  have least := leastNatural.member at rootTwoNumerators with *143  obtain ⟨leastMember, r, rMember, rPositive, rEquation⟩ := rootTwoNumerators.membership.forward with least144  have leastNat := nat.omega.backward with leastMember145  have rNat := nat.omega.backward with rMember146  have descent := rootTwoNumerators.descent at leastNatural(rootTwoNumerators), r with *147  rcases descent with ⟨rIn, rSmaller⟩148  have bound := leastNatural.least at rootTwoNumerators, r with *149  have bad : r < r by arith150  exact Less.irreflexive with *, bad151