-- Uncountability of the Dedekind reals - TailMargin
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.Uncountable.TailMargin
import Cut

-- If the nth digit is zero, every later endpoint stays below the rational
-- lying one numerator unit above that zero digit. The extra summand on the
-- left records a permanent integral margin, so the induction is elementary.
theorem cantorPrefix.zero_tail_margin (X : Set, n k : Nat)
  requires missing : ¬(n ∈ X)
  shows
    (4 ^ succ(n)) * cantorPrefix(X, add(k, succ(n))) + 4 ^ succ(n) ≤
      (4 ^ add(k, succ(n))) * (4 * cantorPrefix(X, n) + 1)
proof
  induction k
  | zero =>
    have indexShape := add.left_unit at succ(n)
    rw indexShape
    have prefixShape := cantorPrefix.succ at X, n
    rw prefixShape
    have digitZero := binaryDigit.zero with missing
    rw digitZero
    have productZero := mul.right_zero at 2
    rw productZero
    have sumZero := add.right_unit at 4 * cantorPrefix(X, n)
    rw sumZero
    have shape : (4 ^ succ(n)) * (4 * cantorPrefix(X, n) + 1) = (4 ^ succ(n)) * (4 * cantorPrefix(X, n)) + 4 ^ succ(n)
      ring
    rw shape
    have total : Nat((4 ^ succ(n)) * (4 * cantorPrefix(X, n)) + 4 ^ succ(n)) by typecheck
    exact LessEqual.reflexive with total
  | succ(j) using ih =>
    have jNatural := h_j
    have nextIndexShape : add(succ(j), succ(n)) = succ(add(j, succ(n))) by simp [add]
    rw nextIndexShape
    have prefixShape := cantorPrefix.succ at X, add(j, succ(n))
    have powerShape := pow.succ at 4, add(j, succ(n))
    rw [prefixShape, powerShape]
    have digitCases := binaryDigit.cases at X, add(j, succ(n))
    have scaled := LessEqual.mul_left at
      (4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))) + 4 ^ succ(n),
      (4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1), 4 with ih
    cases digitCases with digitZero | digitOne
    . rw digitZero
      have productZero := mul.right_zero at 2
      rw productZero
      have sumZero := add.right_unit at 4 * cantorPrefix(X, add(j, succ(n)))
      rw sumZero
      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))
        have oneLeFour : 1 ≤ 4 by arith
        have factorBound := LessEqual.mul_left at 1, 4, 4 ^ succ(n) with oneLeFour
        have commonNatural : Nat(4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))))) by typecheck
        have commonReflexive := LessEqual.reflexive with commonNatural
        have combined := LessEqual.add with commonReflexive, factorBound
        ring_nf at combined
        ring_nf
        exact combined
      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))
        calc
          (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)) := localBound
          _ ≤ 4 * ((4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1)) := scaled
      ring_nf at composed
      ring_nf
      exact composed
    . rw digitOne
      have productOne := mul.right_unit at 2
      rw productOne
      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))
        have twoLeThree : 2 ≤ 3 by arith
        have tailBound := LessEqual.mul_left at 2, 3, 4 ^ succ(n) with twoLeThree
        have powerNatural : Nat(4 ^ succ(n)) by typecheck
        have powerReflexive := LessEqual.reflexive with powerNatural
        have factorBoundRaw := LessEqual.add with powerReflexive, tailBound
        have fourShape := mul.succ_right at 3, 4 ^ succ(n)
        rw ← fourShape at factorBoundRaw
        have factorBound : (4 ^ succ(n)) + (4 ^ succ(n)) * 2 ≤ (4 ^ succ(n)) * 4 by exact factorBoundRaw
        have commonNatural : Nat(4 * ((4 ^ succ(n)) * cantorPrefix(X, add(j, succ(n))))) by typecheck
        have commonReflexive := LessEqual.reflexive with commonNatural
        have combined := LessEqual.add with commonReflexive, factorBound
        ring_nf at combined
        ring_nf
        exact combined
      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))
        calc
          (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)) := localBound
          _ ≤ 4 * ((4 ^ add(j, succ(n))) * (4 * cantorPrefix(X, n) + 1)) := scaled
      ring_nf at composed
      ring_nf
      exact composed