Grace/Cumulus/Real/Uncountable/Separation.g17

Open in Workbench Download source

Imports

TailMargin

Declarations

Source

1-- Uncountability of the Dedekind reals - Separation2-- 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.Uncountable.Separation8import TailMargin910theorem cantorApprox.offset_weak (X : Set, n k : Nat)11  shows cantorApprox(X, n) = cantorApprox(X, add(k, n)) ∨12    relates(rationalLess, cantorApprox(X, n), cantorApprox(X, add(k, n)))13proof14  induction k15  | zero =>16    left17    have shape := add.left_unit at n18    rw shape19    rfl20  | succ(j) using ih =>21    have indexShape : add(succ(j), n) = succ(add(j, n))22      settle with add23    rw indexShape24    have step : cantorApprox(X, add(j, n)) = cantorApprox(X, succ(add(j, n))) ∨ relates(rationalLess, cantorApprox(X, add(j, n)), cantorApprox(X, succ(add(j, n))))25      apply cantorApprox.step_weak at X, add(j, n)26    cases ih with sameStart | lessStart27    . cases step with sameStep | lessStep28      . left29        rw sameStart30        exact sameStep31      . right32        rw sameStart33        exact lessStep34    . cases step with sameStep | lessStep35      . right36        rw ← sameStep37        exact lessStart38      . right39        have startRational : Rational(cantorApprox(X, n))40          apply cantorApprox.rational at X, n41        have middleRational : Rational(cantorApprox(X, add(j, n)))42          apply cantorApprox.rational at X, add(j, n)43        exact rationalLess.transitive at44          cantorApprox(X, n), cantorApprox(X, add(j, n)),45          cantorApprox(X, succ(add(j, n))) with lessStart, lessStep4647def cantorMid (X n : Set) : Set :=48  rationalClass(4 * cantorPrefix(X, n) + 1, 0, 4 ^ succ(n))4950theorem cantorMid.rational (X : Set, n : Nat)51  shows Rational(cantorMid(X, n))52proof53  unfold cantorMid54  have successorNatural : Nat(succ(n)) by typecheck55  apply rationalClass.rational56  . exact pow.four_nonzero with successorNatural5758theorem cantorMid.below_next_of_member (X : Set, n : Nat)59  requires member : n ∈ X60  shows relates(rationalLess, cantorMid(X, n), cantorApprox(X, succ(n)))61proof62  unfold cantorMid63  unfold cantorApprox64  have prefixShape := cantorPrefix.succ at X, n65  have digitOne := binaryDigit.one with member66  rw [prefixShape, digitOne]67  have productOne := mul.right_unit at 268  rw productOne69  have successorNatural : Nat(succ(n)) by typecheck70  have denominatorNonzero : 4 ^ succ(n) ≠ 0 by exact pow.four_nonzero at succ(n) with successorNatural71  apply rationalLess.classes.backward with denominatorNonzero, denominatorNonzero72  have numeratorGap : 4 * cantorPrefix(X, n) + 1 < 4 * cantorPrefix(X, n) + 2 by arith73  have scaled := Less.mul_left with denominatorNonzero, numeratorGap74  ring_nf at scaled75  ring_nf76  exact scaled7778theorem cantorApprox.before_mid (X : Set, n : Nat)79  shows relates(rationalLess, cantorApprox(X, n), cantorMid(X, n))80proof81  unfold cantorApprox82  unfold cantorMid83  have powerShape := pow.succ at 4, n84  rw powerShape85  have oldNonzero := pow.four_nonzero at n with assumption86  have nextNonzero := mul.nonzero at 4, 4 ^ n with87    natural.four_nonzero, oldNonzero88  apply rationalLess.classes.backward at89    cantorPrefix(X, n), 0, 4 ^ n,90    4 * cantorPrefix(X, n) + 1, 0, 4 * (4 ^ n) with91      oldNonzero, nextNonzero92  have remainderNonzero : 4 ^ n ≠ 0 by exact oldNonzero93  have gap := Less.add_positive at94    cantorPrefix(X, n) * ((4 ^ n) * 4), 4 ^ n with remainderNonzero95  ring_nf at gap96  ring_nf97  exact gap9899theorem cantorMid.not_mem_of_missing (X : Set, n : Nat)100  requires missing : ¬(n ∈ X)101  shows ¬(cantorMid(X, n) ∈ cantorReal(X))102proof103  intro inCut104  have shape := cantorReal.membership at X, cantorMid(X, n)105  obtain ⟨midInQ, m, mInOmega, midBelowEndpoint⟩ :=106    shape.forward with inCut107  have mNatural := nat.omega.backward with mInOmega108  have comparison := Less.trichotomy at m, n with mNatural109  cases comparison with mLessN | rest110  . have mLeN := Less.implies_LessEqual with mNatural, mLessN111    obtain ⟨k, kNatural, indexShape⟩ := mLeN112    have commute := add.commutative at k, m with kNatural113    rw commute at indexShape114    have weak : cantorApprox(X, m) = cantorApprox(X, add(k, m)) ∨ relates(rationalLess, cantorApprox(X, m), cantorApprox(X, add(k, m)))115      apply cantorApprox.offset_weak116    rw indexShape at weak117    have endpointBeforeMid : relates(rationalLess, cantorApprox(X, n), cantorMid(X, n))118      apply cantorApprox.before_mid119    cases weak with same | less120    . rw same at midBelowEndpoint121      have cycle := rationalLess.transitive with midBelowEndpoint, endpointBeforeMid122      have irreflexive := rationalLess.irreflexive_on123      exact irreflexive with cantorMid(X, n), midInQ, cycle124    . have midBelowN := rationalLess.transitive at125        cantorMid(X, n), cantorApprox(X, m), cantorApprox(X, n) with126          midBelowEndpoint, less127      have cycle := rationalLess.transitive with midBelowN, endpointBeforeMid128      have irreflexive := rationalLess.irreflexive_on129      exact irreflexive with cantorMid(X, n), midInQ, cycle130  . cases rest with equal | nLessM131    . rw equal at midBelowEndpoint132      have endpointBeforeMid : relates(rationalLess, cantorApprox(X, n), cantorMid(X, n))133        apply cantorApprox.before_mid134      have cycle := rationalLess.transitive with midBelowEndpoint, endpointBeforeMid135      have irreflexive := rationalLess.irreflexive_on136      exact irreflexive with cantorMid(X, n), midInQ, cycle137      obtain ⟨j, jNatural, tailIndexShape⟩ := nLessM138      have commute := add.commutative at j, succ(n) with jNatural139      rw commute at tailIndexShape140      have margin : (4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))) + 4 ^ succ(n) ≤ (4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1)141        apply cantorPrefix.zero_tail_margin142        . exact missing143      rw tailIndexShape at margin144      have successorNatural : Nat(succ(n)) by typecheck145      have midNonzero := pow.four_nonzero with successorNatural146      have endpointNonzero := pow.four_nonzero with mNatural147      unfold cantorMid at midBelowEndpoint148      unfold cantorApprox at midBelowEndpoint149      have cross := rationalLess.classes.forward with midNonzero, endpointNonzero, midBelowEndpoint150      ring_nf at cross151      have crossClean : (4 ^ m) * (4 * cantorPrefix(X, n) + 1) < (4 ^ succ(n)) * cantorPrefix(X, m)152        ring_nf153        exact cross154      have baseLeMargin : (4 ^ succ(n)) * cantorPrefix(X, m) ≤ (4 ^ succ(n)) * cantorPrefix(X, m) + 4 ^ succ(n)155        apply LessEqual.add_right156      have weakMargin := LessEqual.transitive with baseLeMargin, margin157      have reverseStrict := Less.transitive_LessEqual with crossClean, weakMargin158      exact Less.irreflexive with reverseStrict159160theorem cantorReal.bit (X : Set, n : Nat)161  shows n ∈ X ↔ cantorMid(X, n) ∈ cantorReal(X)162proof163  constructor164  . intro member165    have midRational : Rational(cantorMid(X, n)) by apply cantorMid.rational at X, n166    have belowNext : relates(rationalLess, cantorMid(X, n), cantorApprox(X, succ(n)))167      apply cantorMid.below_next_of_member168      . exact member169    have successorNatural : Nat(succ(n)) by typecheck170    have successorInOmega := nat.omega.forward with successorNatural171    have shape := cantorReal.membership at X, cantorMid(X, n)172    apply shape.backward173    constructor174      exact midRational175    . refine ⟨succ(n), successorInOmega, belowNext⟩176  . intro midpointMember177    by_contra missing178    exact cantorMid.not_mem_of_missing with missing, midpointMember179