Grace/Cumulus/Real/Uncountable/Digits.g17

Open in Workbench Download source

Imports

Nat.Pow · Set

Declarations

Source

1-- Uncountability of the Dedekind reals - Digits2-- 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.Digits8import Nat.Pow9import Set1011-- The membership bit of n in X, represented as a von Neumann natural. The12-- bounded separation is either {1} or empty, so its union is respectively13-- 1 or 0, so the construction stays inside set theory.14def binaryDigitSet (X n : Set) : Set :=15  { d ∈ {1} | n ∈ X }16def binaryDigitRaw (X n : Set) : Set := ⋃(binaryDigitSet(X, n))1718theorem binaryDigitRaw.one (X n : Set)19  requires member : n ∈ X20  shows binaryDigitRaw(X, n) = 121proof22  unfold binaryDigitRaw23  ext x24  simp [set.union, binaryDigitSet, singleton.membership, member]2526theorem binaryDigitRaw.zero (X n : Set)27  requires missing : ¬(n ∈ X)28  shows binaryDigitRaw(X, n) = 029proof30  unfold binaryDigitRaw31  ext x32  simp [set.union, binaryDigitSet, singleton.membership, missing, nat.zero, set.empty]3334theorem binaryDigitRaw.cases (X n : Set)35  shows binaryDigitRaw(X, n) = 0 ∨ binaryDigitRaw(X, n) = 136proof37  have membershipCases : n ∈ X ∨ ¬(n ∈ X) by tauto38  cases membershipCases with member | missing39  . right40    exact binaryDigitRaw.one with member41  . left42    exact binaryDigitRaw.zero with missing4344instance binaryDigitRaw.natural (X n : Set)45  shows Nat(binaryDigitRaw(X, n))46proof47  have cases := binaryDigitRaw.cases at X, n48  cases cases with zero | one49  . rw zero50    exact Naturals.constructor.zero51  . rw one52    typecheck5354def binaryDigit (X n : Set) : Nat := binaryDigitRaw(X, n)5556theorem binaryDigit.zero (X n : Set)57  requires missing : ¬(n ∈ X)58  shows binaryDigit(X, n) = 059proof60  unfold binaryDigit61  exact binaryDigitRaw.zero with missing6263theorem binaryDigit.one (X n : Set)64  requires member : n ∈ X65  shows binaryDigit(X, n) = 166proof67  unfold binaryDigit68  exact binaryDigitRaw.one with member6970theorem binaryDigit.cases (X n : Set)71  shows binaryDigit(X, n) = 0 ∨ binaryDigit(X, n) = 172proof73  have cases := binaryDigitRaw.cases at X, n74  cases cases with zero | one75  . left76    simp [binaryDigit]77  . right78    simp [binaryDigit]7980theorem binaryDigit.natural (X n : Set)81  shows Nat(binaryDigit(X, n))82proof83  unfold binaryDigit84  exact binaryDigitRaw.natural8586-- Base-four prefixes with digits 0 and 2. The gap between those digits is87-- what makes the eventual real recover every membership bit uniquely.88def cantorPrefix (X : Set, n : Nat) → Nat89  | X, zero => 090  | X, succ(n) => 4 * cantorPrefix(X, n) + 2 * binaryDigit(X, n)9192theorem cantorPrefix.zero (X : Set)93  shows cantorPrefix(X, 0) = 094proof95  simp [cantorPrefix]9697theorem cantorPrefix.succ (X : Set, n : Nat)98  shows cantorPrefix(X, succ(n)) =99    4 * cantorPrefix(X, n) + 2 * binaryDigit(X, n)100proof101  simp [cantorPrefix]102103theorem cantorPrefix.natural (X : Set, n : Nat)104  shows Nat(cantorPrefix(X, n))105proof106  induction n107  | zero =>108    have shape := cantorPrefix.zero at X109    rw shape110    typecheck111  | succ(k) using ih =>112    have shape := cantorPrefix.succ at X, k113    rw shape114    have digitNatural := binaryDigit.natural at X, k115    have rightNatural := mul.closed at binaryDigit(X, k), 2 with digitNatural116    exact add.closed with rightNatural117118theorem pow.four_nonzero (n : Nat)119  shows 4 ^ n ≠ 0120proof121  induction n122  | zero =>123    have shape := pow.zero at 4124    rw shape125    intro equal126    have impossible := Naturals.disjoint.zero.succ at 0127    apply impossible128    rw equal129    rfl130  | succ(k) using ih =>131    have shape := pow.succ at 4, k132    rw shape133    have fourNonzero : 4 ≠ 0134      intro fourZero135      have zeroFour : 0 = 4136        rw fourZero137        rfl138      have impossible := Naturals.disjoint.zero.succ at 3139      exact impossible with zeroFour140    exact mul.nonzero with fourNonzero, ih141142theorem natural.four_nonzero143  shows 4 ≠ 0144proof145  intro fourZero146  have zeroFour : 0 = 4147    rw fourZero148    rfl149  have impossible := Naturals.disjoint.zero.succ at 3150  exact impossible with zeroFour151