-- The real square root of two is not rational
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.RootTwoRational
import RationalEmbedding
import RootTwo
import NumberTheory.RootTwo

theorem sqrtTwo.square_scaled (m : Nat)
  shows (√2 * realNat(m)) * (√2 * realNat(m)) = (2:R) * (realNat(m) * realNat(m))
proof
  have one := realZero.lt_one
  have twoLe : (0:R) ≤ (2:R) by linarith
  have twoNonnegative := NonnegativeReal.of_le with *
  have square := sqrt.square with *
  have expand : (√2 * realNat(m)) * (√2 * realNat(m)) = (√2 * √2) * (realNat(m) * realNat(m)) by ring
  rw [expand, square]
  rfl

-- (√2 · m)² is never the square of a natural number when m is positive.
theorem sqrtTwo.scaled_square_ne (d m : Nat)
  requires nonzero : m ≠ 0
  shows (√2 * realNat(m)) * (√2 * realNat(m)) ≠ realNat(d) * realNat(d)
proof
  intro equal
  have scaled := sqrtTwo.square_scaled at m with *
  rw scaled at equal
  have left : realNat(2 * (m * m)) = (2:R) * (realNat(m) * realNat(m))
    rw [realNat.mul, realNat.mul, realNat.two]
    rfl
  have right : realNat(d * d) = realNat(d) * realNat(d)
    exact realNat.mul with *
  have natural : realNat(2 * (m * m)) = realNat(d * d) by rwa [left, right]
  have equalNaturals := realNat.injective with *
  have contradiction := rootTwo.irrational at d, m with *
  symm at equalNaturals
  exact contradiction with equalNaturals

-- √2 is not the cut of any rational. A rational is (a − b)/m with m positive,
-- so √2 · m would be the difference of two naturals, and its square the square
-- of a natural.
theorem sqrtTwo.ne_rationalCut (q : Rational)
  shows √2 ≠ rationalCut(q)
proof
  intro equal
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates at q with *
  have scaled := rationalCut.scaled at a, b, m with *
  rw [← qShape, ← equal] at scaled
  have one := realZero.lt_one
  have twoLe : (0:R) ≤ (2:R) by linarith
  have twoNonnegative := NonnegativeReal.of_le with *
  have shape := LessEqual.total at a, b with *
  cases shape with le | ge
  . obtain ⟨d, dNat, equation⟩ := le
    have expand : realNat(b) = (realNat(a):R) + (realNat(d):R)
      rw [← equation, realNat.add]
      rfl
    have squares : (√2 * realNat(m)) * (√2 * realNat(m)) = realNat(d) * realNat(d)
      rw [scaled, expand]
      ring
    exact sqrtTwo.scaled_square_ne with *, squares
  . obtain ⟨d, dNat, equation⟩ := ge
    have expand : realNat(a) = (realNat(b):R) + (realNat(d):R)
      rw [← equation, realNat.add]
      rfl
    have squares : (√2 * realNat(m)) * (√2 * realNat(m)) = realNat(d) * realNat(d)
      rw [scaled, expand]
      ring
    exact sqrtTwo.scaled_square_ne with *, squares