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

-- The real coded by X is the lower closure of all its finite endpoints.
def cantorReal (X : Set) : Set :=
  { q ∈ ℚ | ∃ n ∈ ℕ, relates(rationalLess, q, cantorApprox(X, n)) }

theorem cantorReal.real (X : Set)
  shows Real(cantorReal(X))
proof
  apply Real.characterization.backward
  constructor
    intros q member
    have shape := cantorReal.membership at X, q
    obtain ⟨qRational, witnessData⟩ := shape.forward with member
    exact qRational
  constructor
  . have zeroRational := rationalZero.rational
    obtain ⟨below, belowRational, belowZero⟩ := rationalLess.exists_below with zeroRational
    witness below
    have shape := cantorReal.membership at X, below
    apply shape.backward
    constructor
    . exact belowRational
    . witness 0
      constructor
      . exact nat.omega.forward at 0 with Naturals.constructor.zero
      . rw cantorApprox.zero
        exact belowZero
  constructor
  . intro allRationals
    have oneInCut : rationalOne ∈ cantorReal(X)
      rw allRationals
      exact rationalOne.rational
    have oneShape := cantorReal.membership at X, rationalOne
    obtain ⟨oneRationalAgain, n, nNatural, oneBelow⟩ :=
      oneShape.forward with oneInCut
    have nNat := nat.omega.backward with nNatural
    have endpointBelowOne : cantorApprox(X, n) < rationalOne by apply cantorApprox.below_one
    have cycle := rationalLess.transitive with oneBelow, endpointBelowOne
    have irreflexive := rationalLess.irreflexive_on
    exact irreflexive with rationalOne, oneRationalAgain, cycle
  constructor
  . intros q qInCut p pRational pBelowQ
    have qShape := cantorReal.membership at X, q
    obtain ⟨qRational, m, mNatural, qBelowEndpoint⟩ :=
      qShape.forward with qInCut
    have mNat := nat.omega.backward with mNatural
    have pBelowEndpoint := rationalLess.transitive with pBelowQ, qBelowEndpoint
    have pShape := cantorReal.membership at X, p
    apply pShape.backward
    constructor
    . exact pRational
    . refine ⟨m, mNatural, pBelowEndpoint⟩
  . intros q qInCut
    have qShape := cantorReal.membership at X, q
    obtain ⟨qRationalAgain, k, kNatural, qBelowEndpointAgain⟩ :=
      qShape.forward with qInCut
    have kNat := nat.omega.backward with kNatural
    have endpointRationalK : Rational(cantorApprox(X, k)) by apply cantorApprox.rational
    have qRationalClass : Rational(q) by exact qRationalAgain
    obtain ⟨r, rRational, qBelowR, rBelowEndpoint⟩ := rationalLess.dense with
      qRationalClass, endpointRationalK, qBelowEndpointAgain
    witness r
    constructor
    . have rShape := cantorReal.membership at X, r
      apply rShape.backward
      constructor
      . exact rRational
      . refine ⟨k, kNatural, rBelowEndpoint⟩
    . exact qBelowR