-- Uncountability of the Dedekind reals - Approximation
-- 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.Uncountable.Approximation
import PrefixBound
import Squares

-- The nth rational endpoint is the finite base-four expansion encoded by the
-- first n membership bits of X.
def cantorApprox (X n : Set) : Set :=
  rationalClass(cantorPrefix(X, n), 0, 4 ^ n)

theorem cantorApprox.rational (X : Set, n : Nat)
  shows Rational(cantorApprox(X, n))
proof
  unfold cantorApprox
  have powerNonzero : 4 ^ n ≠ 0 by exact pow.four_nonzero at n with assumption
  apply rationalClass.rational
  . exact powerNonzero

theorem cantorApprox.zero (X : Set)
  shows cantorApprox(X, 0) = rationalZero
proof
  unfold cantorApprox
  have prefixShape := cantorPrefix.zero at X
  have powerShape := pow.zero at 4
  rw [prefixShape, powerShape]
  unfold rationalZero
  rfl

theorem cantorApprox.below_one (X : Set, n : Nat)
  shows cantorApprox(X, n) < rationalOne
proof
  unfold cantorApprox
  unfold rationalOne
  have powerNonzero : 4 ^ n ≠ 0 by exact pow.four_nonzero at n with assumption
  have oneNonzero : 1 ≠ 0
    intro oneZero
    have zeroNotOne := Naturals.disjoint.zero.succ at 0
    apply zeroNotOne
    rw oneZero
    rfl
  apply rationalLess.classes.backward with powerNonzero, oneNonzero
  have bound := cantorPrefix.lt_pow at X, n
  ring_nf
  exact bound

theorem cantorApprox.step_weak (X : Set, n : Nat)
  shows cantorApprox(X, n) = cantorApprox(X, succ(n)) ∨
    relates(rationalLess, cantorApprox(X, n), cantorApprox(X, succ(n)))
proof
  have prefixShape := cantorPrefix.succ at X, n
  have powerShape := pow.succ at 4, n
  have digitCases := binaryDigit.cases at X, n
  have powerNonzero : 4 ^ n ≠ 0 by exact pow.four_nonzero at n with assumption
  have nextPowerNonzero : 4 * (4 ^ n) ≠ 0 by exact mul.nonzero at 4, 4 ^ n with natural.four_nonzero, powerNonzero
  cases digitCases with zero | one
  . left
    unfold cantorApprox
    rw [prefixShape, powerShape, zero]
    have productZero := mul.right_zero at 2
    rw productZero
    have sumZero := add.right_unit at 4 * cantorPrefix(X, n)
    rw sumZero
    apply rationalClass.eq with powerNonzero, nextPowerNonzero
    ring
  . right
    unfold cantorApprox
    rw [prefixShape, powerShape, one]
    have productOne := mul.right_unit at 2
    rw productOne
    apply rationalLess.classes.backward with powerNonzero, nextPowerNonzero
    have twoNonzero : 2 ≠ 0
      intro twoZero
      have zeroNotTwo := Naturals.disjoint.zero.succ at 1
      apply zeroNotTwo
      rw twoZero
      rfl
    have remainderNonzero := mul.nonzero with powerNonzero, twoNonzero
    have augmented := Less.add_positive at
      cantorPrefix(X, n) * ((4 ^ n) * 4), (4 ^ n) * 2 with
        remainderNonzero
    ring_nf
    ring_nf at augmented
    exact augmented