Grace/Cumulus/Real/Archimedean.g17

Open in Workbench Download source

Imports

Core

Declarations

Source

1-- Archimedean boundary approximation for Dedekind cuts2-- 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.Real.Archimedean8import Core910-- Natural indices whose points on a fixed rational grid belong to A.11-- This helper is local to the construction; the public boundary theorem12-- below speaks only the language of rational addition.13def cutGridIndices (A : Set) (a b n D : Nat) : Set :=14  { k ∈ ℕ | rationalGrid(a, b, n, D, k) ∈ A }1516-- A Dedekind cut has a member within every positive rational distance of its17-- complement.  This is the endpoint-free boundary principle used throughout18-- the algebra and, later, in epsilon arguments for real analysis.19theorem DedekindCut.exists_boundary_within (A : Set, ε : Rational)20  requires cut : DedekindCut(A)21  requires positive : rationalZero < ε22  shows ∃ p, Rational(p) ∧ p ∈ A ∧ ¬(rationalAddValue(p, ε) ∈ A)23proof24  obtain ⟨a0, a0InA⟩ := DedekindCut.nonempty with cut25  have subsetA := DedekindCut.subset_rationals with cut26  have a0Rational : Rational(a0)27    unfold Rational28    exact subsetA with a0, a0InA29  obtain ⟨a, aNatural, b, bNatural, n, nNatural, nNonzero, a0Shape⟩ := Rational.coordinates with a0Rational3031  have properA := DedekindCut.proper with cut32  obtain ⟨u, uInQ, uMissing⟩ := ProperSubset.missing with properA33  have uRational : Rational(u) by exact uInQ3435  obtain ⟨D, DNatural, DNonzero, stepPositive, stepSmall⟩ := rationalLess.exists_positive_unit_fraction with36    positive37  have stepRational := rationalClass.rational at 1, 0, D with DNonzero3839  have gapRational := rationalSubValue.rational with uRational, a0Rational40  obtain ⟨N, NNatural, gapBelowN⟩ := Rational.below_natural with gapRational41  have oneNatural : Nat(1) by typecheck42  have oneNonzero : 1 ≠ 043    intro oneZero44    arith45  have naturalRational := rationalClass.rational with46    NNatural, Naturals.constructor.zero, oneNatural, oneNonzero47  have uBelowFar := rationalLess.add_left_of_sub_left with uRational, a0Rational, gapBelowN4849  have zeroInIndices : 0 ∈ cutGridIndices(A, a, b, n, D)50    have zeroMembership := cutGridIndices.membership at A, a, b, n, D, 051    apply zeroMembership.backward52    constructor53    . exact Naturals.constructor.zero54    . have gridZero := rationalGrid.zero at a, b, n, D with55        nNonzero, DNonzero56      rwa [gridZero, ← a0Shape]5758  have farMissing : ¬(D * N ∈ cutGridIndices(A, a, b, n, D))59    intro farInIndices60    have farMembership := cutGridIndices.membership at61      A, a, b, n, D, D * N62    obtain ⟨farNatural, farInA⟩ := farMembership.forward with farInIndices63    have farShape := rationalGrid.natural_step at a, b, n, D, N with64      nNonzero, DNonzero65    rw [a0Shape, rationalAddValue.notation, ← farShape] at uBelowFar66    have uInA := DedekindCut.downward with cut, farInA, uInQ, uBelowFar67    exact uMissing with uInA6869  have endpointNatural : Nat(D * N) by typecheck70  obtain ⟨k, kNatural, kInIndices, successorMissing⟩ := natural.exists_boundary with71    endpointNatural, zeroInIndices, farMissing72  have kMembership := cutGridIndices.membership at73    A, a, b, n, D, k74  obtain ⟨kNaturalAgain, gridInA⟩ := kMembership.forward with kInIndices7576  witness rationalGrid(a, b, n, D, k)77  constructor78  . exact rationalGrid.rational with nNonzero, DNonzero79  constructor80  . exact gridInA81  . intro shiftedInA82    have gridRational := rationalGrid.rational at a, b, n, D, k with83      nNonzero, DNonzero84    have shiftedLess := rationalLess.add_left at85      rationalClass(1, 0, D), ε, rationalGrid(a, b, n, D, k) with86      stepRational, assumption, gridRational, stepSmall87    rw [rationalAddValue.notation, rationalAddValue.notation] at shiftedLess88    have shiftedRational := rationalAddValue.rational_raw at89      rationalGrid(a, b, n, D, k), ε with gridRational, assumption90    have smallShiftRational := rationalAddValue.rational_raw with gridRational, stepRational91    have smallShiftInA := DedekindCut.downward at92      A,93      rationalAddValue(rationalGrid(a, b, n, D, k), rationalClass(1, 0, D)),94      rationalAddValue(rationalGrid(a, b, n, D, k), ε) with95      cut, shiftedInA, smallShiftRational,96      shiftedLess97    have successorInIndices : succ(k) ∈ cutGridIndices(A, a, b, n, D)98      have successorMembership := cutGridIndices.membership at99        A, a, b, n, D, succ(k)100      apply successorMembership.backward101      constructor102      . exact Naturals.constructor.succ at k with kNatural103      . have successorShape := rationalGrid.successor at104          a, b, n, D, k with nNonzero, DNonzero105        rwa successorShape106    exact successorMissing with successorInIndices107