-- Archimedean boundary approximation for Dedekind cuts
-- 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.Archimedean
import Core

-- Natural indices whose points on a fixed rational grid belong to A.
-- This helper is local to the construction; the public boundary theorem
-- below speaks only the language of rational addition.
def cutGridIndices (A : Set) (a b n D : Nat) : Set :=
  { k ∈ ℕ | rationalGrid(a, b, n, D, k) ∈ A }

-- A Dedekind cut has a member within every positive rational distance of its
-- complement.  This is the endpoint-free boundary principle used throughout
-- the algebra and, later, in epsilon arguments for real analysis.
theorem DedekindCut.exists_boundary_within (A : Set, ε : Rational)
  requires cut : DedekindCut(A)
  requires positive : rationalZero < ε
  shows ∃ p, Rational(p) ∧ p ∈ A ∧ ¬(rationalAddValue(p, ε) ∈ A)
proof
  obtain ⟨a0, a0InA⟩ := DedekindCut.nonempty with cut
  have subsetA := DedekindCut.subset_rationals with cut
  have a0Rational : Rational(a0)
    unfold Rational
    exact subsetA with a0, a0InA
  obtain ⟨a, aNatural, b, bNatural, n, nNatural, nNonzero, a0Shape⟩ := Rational.coordinates with a0Rational

  have properA := DedekindCut.proper with cut
  obtain ⟨u, uInQ, uMissing⟩ := ProperSubset.missing with properA
  have uRational : Rational(u) by exact uInQ

  obtain ⟨D, DNatural, DNonzero, stepPositive, stepSmall⟩ := rationalLess.exists_positive_unit_fraction with
    positive
  have stepRational := rationalClass.rational at 1, 0, D with DNonzero

  have gapRational := rationalSubValue.rational with uRational, a0Rational
  obtain ⟨N, NNatural, gapBelowN⟩ := Rational.below_natural with gapRational
  have oneNatural : Nat(1) by typecheck
  have oneNonzero : 1 ≠ 0
    intro oneZero
    arith
  have naturalRational := rationalClass.rational with
    NNatural, Naturals.constructor.zero, oneNatural, oneNonzero
  have uBelowFar := rationalLess.add_left_of_sub_left with uRational, a0Rational, gapBelowN

  have zeroInIndices : 0 ∈ cutGridIndices(A, a, b, n, D)
    have zeroMembership := cutGridIndices.membership at A, a, b, n, D, 0
    apply zeroMembership.backward
    constructor
    . exact Naturals.constructor.zero
    . have gridZero := rationalGrid.zero at a, b, n, D with
        nNonzero, DNonzero
      rwa [gridZero, ← a0Shape]

  have farMissing : ¬(D * N ∈ cutGridIndices(A, a, b, n, D))
    intro farInIndices
    have farMembership := cutGridIndices.membership at
      A, a, b, n, D, D * N
    obtain ⟨farNatural, farInA⟩ := farMembership.forward with farInIndices
    have farShape := rationalGrid.natural_step at a, b, n, D, N with
      nNonzero, DNonzero
    rw [a0Shape, rationalAddValue.notation, ← farShape] at uBelowFar
    have uInA := DedekindCut.downward with cut, farInA, uInQ, uBelowFar
    exact uMissing with uInA

  have endpointNatural : Nat(D * N) by typecheck
  obtain ⟨k, kNatural, kInIndices, successorMissing⟩ := natural.exists_boundary with
    endpointNatural, zeroInIndices, farMissing
  have kMembership := cutGridIndices.membership at
    A, a, b, n, D, k
  obtain ⟨kNaturalAgain, gridInA⟩ := kMembership.forward with kInIndices

  witness rationalGrid(a, b, n, D, k)
  constructor
  . exact rationalGrid.rational with nNonzero, DNonzero
  constructor
  . exact gridInA
  . intro shiftedInA
    have gridRational := rationalGrid.rational at a, b, n, D, k with
      nNonzero, DNonzero
    have shiftedLess := rationalLess.add_left at
      rationalClass(1, 0, D), ε, rationalGrid(a, b, n, D, k) with
      stepRational, assumption, gridRational, stepSmall
    rw [rationalAddValue.notation, rationalAddValue.notation] at shiftedLess
    have shiftedRational := rationalAddValue.rational_raw at
      rationalGrid(a, b, n, D, k), ε with gridRational, assumption
    have smallShiftRational := rationalAddValue.rational_raw with gridRational, stepRational
    have smallShiftInA := DedekindCut.downward at
      A,
      rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D)),
      rationalAddValue(rationalGrid(a, b, n, D, k), ε) with
      cut, shiftedInA, smallShiftRational,
      shiftedLess
    have successorInIndices : succ(k) ∈ cutGridIndices(A, a, b, n, D)
      have successorMembership := cutGridIndices.membership at
        A, a, b, n, D, succ(k)
      apply successorMembership.backward
      constructor
      . exact Naturals.constructor.succ at k with kNatural
      . have successorShape := rationalGrid.successor at
          a, b, n, D, k with nNonzero, DNonzero
        rwa successorShape
    exact successorMissing with successorInIndices