Grace/Cumulus/Real/Uncountable/Approximation.g17

Open in Workbench Download source

Imports

PrefixBound · Squares

Declarations

Source

1-- Uncountability of the Dedekind reals - Approximation2-- 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.Approximation8import PrefixBound9import Squares1011-- The nth rational endpoint is the finite base-four expansion encoded by the12-- first n membership bits of X.13def cantorApprox (X n : Set) : Set :=14  rationalClass(cantorPrefix(X, n), 0, 4 ^ n)1516theorem cantorApprox.rational (X : Set, n : Nat)17  shows Rational(cantorApprox(X, n))18proof19  unfold cantorApprox20  have powerNonzero : 4 ^ n ≠ 0 by exact pow.four_nonzero at n with assumption21  apply rationalClass.rational22  . exact powerNonzero2324theorem cantorApprox.zero (X : Set)25  shows cantorApprox(X, 0) = rationalZero26proof27  unfold cantorApprox28  have prefixShape := cantorPrefix.zero at X29  have powerShape := pow.zero at 430  rw [prefixShape, powerShape]31  unfold rationalZero32  rfl3334theorem cantorApprox.below_one (X : Set, n : Nat)35  shows cantorApprox(X, n) < rationalOne36proof37  unfold cantorApprox38  unfold rationalOne39  have powerNonzero : 4 ^ n ≠ 0 by exact pow.four_nonzero at n with assumption40  have oneNonzero : 1 ≠ 041    intro oneZero42    have zeroNotOne := Naturals.disjoint.zero.succ at 043    apply zeroNotOne44    rw oneZero45    rfl46  apply rationalLess.classes.backward with powerNonzero, oneNonzero47  have bound := cantorPrefix.lt_pow at X, n48  ring_nf49  exact bound5051theorem cantorApprox.step_weak (X : Set, n : Nat)52  shows cantorApprox(X, n) = cantorApprox(X, succ(n)) ∨53    relates(rationalLess, cantorApprox(X, n), cantorApprox(X, succ(n)))54proof55  have prefixShape := cantorPrefix.succ at X, n56  have powerShape := pow.succ at 4, n57  have digitCases := binaryDigit.cases at X, n58  have powerNonzero : 4 ^ n ≠ 0 by exact pow.four_nonzero at n with assumption59  have nextPowerNonzero : 4 * (4 ^ n) ≠ 0 by exact mul.nonzero at 4, 4 ^ n with natural.four_nonzero, powerNonzero60  cases digitCases with zero | one61  . left62    unfold cantorApprox63    rw [prefixShape, powerShape, zero]64    have productZero := mul.right_zero at 265    rw productZero66    have sumZero := add.right_unit at 4 * cantorPrefix(X, n)67    rw sumZero68    apply rationalClass.eq with powerNonzero, nextPowerNonzero69    ring70  . right71    unfold cantorApprox72    rw [prefixShape, powerShape, one]73    have productOne := mul.right_unit at 274    rw productOne75    apply rationalLess.classes.backward with powerNonzero, nextPowerNonzero76    have twoNonzero : 2 ≠ 077      intro twoZero78      have zeroNotTwo := Naturals.disjoint.zero.succ at 179      apply zeroNotTwo80      rw twoZero81      rfl82    have remainderNonzero := mul.nonzero with powerNonzero, twoNonzero83    have augmented := Less.add_positive at84      cantorPrefix(X, n) * ((4 ^ n) * 4), (4 ^ n) * 2 with85        remainderNonzero86    ring_nf87    ring_nf at augmented88    exact augmented89