Grace/Cumulus/Real/Uncountable/TailMargin.g17

Open in Workbench Download source

Imports

Cut

Declarations

Source

1-- Uncountability of the Dedekind reals - TailMargin2-- 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.TailMargin8import Cut910-- If the nth digit is zero, every later endpoint stays below the rational11-- lying one numerator unit above that zero digit. The extra summand on the12-- left records a permanent integral margin, so the induction is elementary.13theorem cantorPrefix.zero_tail_margin (X : Set, n k : Nat)14  requires missing : ¬(n ∈ X)15  shows16    (4 ^ succ(n)) * cantorPrefix(X, add(k, succ(n))) + 4 ^ succ(n) ≤17      (4 ^ add(k, succ(n))) * (4 * cantorPrefix(X, n) + 1)18proof19  induction k20  | zero =>21    have indexShape := add.left_unit at succ(n)22    rw indexShape23    have prefixShape := cantorPrefix.succ at X, n24    rw prefixShape25    have digitZero := binaryDigit.zero with missing26    rw digitZero27    have productZero := mul.right_zero at 228    rw productZero29    have sumZero := add.right_unit at 4 * cantorPrefix(X, n)30    rw sumZero31    have shape : (4 ^ succ(n)) * (4 * cantorPrefix(X, n) + 1) = (4 ^ succ(n)) * (4 * cantorPrefix(X, n)) + 4 ^ succ(n)32      ring33    rw shape34    have total : Nat((4 ^ succ(n)) * (4 * cantorPrefix(X, n)) + 4 ^ succ(n)) by typecheck35    exact LessEqual.reflexive with total36  | succ(j) using ih =>37    have jNatural := h_j38    have nextIndexShape : add(succ(j), succ(n)) = succ(add(j, succ(n))) by simp [add]39    rw nextIndexShape40    have prefixShape := cantorPrefix.succ at X, add(j, succ(n))41    have powerShape := pow.succ at 4, add(j, succ(n))42    rw [prefixShape, powerShape]43    have digitCases := binaryDigit.cases at X, add(j, succ(n))44    have scaled := LessEqual.mul_left at45      (4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))) + 4 ^ succ(n),46      (4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1), 4 with ih47    cases digitCases with digitZero | digitOne48    . rw digitZero49      have productZero := mul.right_zero at 250      rw productZero51      have sumZero := add.right_unit at 4 * cantorPrefix(X, add(j, succ(n)))52      rw sumZero53      have localBound : (4 ^ succ(n)) * (4 * cantorPrefix(X, add(j, succ(n)))) + 4 ^ succ(n) ≤ 4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))) + 4 ^ succ(n))54        have oneLeFour : 1 ≤ 4 by arith55        have factorBound := LessEqual.mul_left at 1, 4, 4 ^ succ(n) with oneLeFour56        have commonNatural : Nat(4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))))) by typecheck57        have commonReflexive := LessEqual.reflexive with commonNatural58        have combined := LessEqual.add with commonReflexive, factorBound59        ring_nf at combined60        ring_nf61        exact combined62      have composed : (4 ^ succ(n)) * (4 * cantorPrefix(X, add(j, succ(n)))) + 4 ^ succ(n) ≤ 4 * ((4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1))63        calc64          (4 ^ succ(n)) * (4 * cantorPrefix(X, add(j, succ(n)))) + 4 ^ succ(n) ≤ 4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))) + 4 ^ succ(n)) := localBound65          _ ≤ 4 * ((4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1)) := scaled66      ring_nf at composed67      ring_nf68      exact composed69    . rw digitOne70      have productOne := mul.right_unit at 271      rw productOne72      have localBound : (4 ^ succ(n)) * (4 * cantorPrefix(X, add(j, succ(n))) + 2) + 4 ^ succ(n) ≤ 4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))) + 4 ^ succ(n))73        have twoLeThree : 2 ≤ 3 by arith74        have tailBound := LessEqual.mul_left at 2, 3, 4 ^ succ(n) with twoLeThree75        have powerNatural : Nat(4 ^ succ(n)) by typecheck76        have powerReflexive := LessEqual.reflexive with powerNatural77        have factorBoundRaw := LessEqual.add with powerReflexive, tailBound78        have fourShape := mul.succ_right at 3, 4 ^ succ(n)79        rw ← fourShape at factorBoundRaw80        have factorBound : (4 ^ succ(n)) + (4 ^ succ(n)) * 2 ≤ (4 ^ succ(n)) * 4 by exact factorBoundRaw81        have commonNatural : Nat(4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))))) by typecheck82        have commonReflexive := LessEqual.reflexive with commonNatural83        have combined := LessEqual.add with commonReflexive, factorBound84        ring_nf at combined85        ring_nf86        exact combined87      have composed : (4 ^ succ(n)) * (4 * cantorPrefix(X, add(j, succ(n))) + 2) + 4 ^ succ(n) ≤ 4 * ((4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1))88        calc89          (4 ^ succ(n)) * (4 * cantorPrefix(X, add(j, succ(n))) + 2) + 4 ^ succ(n) ≤ 4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))) + 4 ^ succ(n)) := localBound90          _ ≤ 4 * ((4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1)) := scaled91      ring_nf at composed92      ring_nf93      exact composed94