-- Uncountability of the Dedekind reals - PrefixBound
-- 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.PrefixBound
import Digits
import Nat.Order

theorem cantorPrefix.lt_pow (X : Set, n : Nat)
  shows cantorPrefix(X, n) < 4 ^ n
proof
  induction n
  | zero =>
    have prefixShape := cantorPrefix.zero at X
    have powerShape := pow.zero at 4
    rw prefixShape
    rw powerShape
    arith
  | succ(k) using ih =>
    have prefixShape := cantorPrefix.succ at X, k
    have powerShape := pow.succ at 4, k
    rw prefixShape
    rw powerShape
    have digitCases := binaryDigit.cases at X, k
    cases digitCases with zero | one
    . rw zero
      have productZero := mul.right_zero at 2
      rw productZero
      have sumZero := add.right_unit at 4 * cantorPrefix(X, k)
      rw sumZero
      exact Less.mul_left at cantorPrefix(X, k), 4 ^ k, 4 with
        natural.four_nonzero, ih
    . rw one
      have productOne := mul.right_unit at 2
      rw productOne
      have prefixNatural : Nat(cantorPrefix(X, k))
        apply cantorPrefix.natural at X, k
      have fourNatural : Nat(4)
        typecheck
      have powerNatural : Nat(4 ^ k)
        apply pow.closed at 4, k
      have leftNatural : Nat(4 * cantorPrefix(X, k))
        typecheck
      have rightNatural : Nat(4 * (4 ^ k))
        typecheck
      have leftReflexive : 4 * cantorPrefix(X, k) ≤ 4 * cantorPrefix(X, k)
        apply LessEqual.reflexive at 4 * cantorPrefix(X, k)
      have twoLessFour : 2 < 4
        arith
      have gap : 4 * cantorPrefix(X, k) + 2 < 4 * cantorPrefix(X, k) + 4
        apply LessEqual.add_Less at
          4 * cantorPrefix(X, k), 4 * cantorPrefix(X, k), 2, 4
        . exact leftReflexive
        . exact twoLessFour
      have successorBound := ih
      have scaledBound : LessEqual(mul(4, succ(cantorPrefix(X, k))), mul(4, 4 ^ k))
        apply LessEqual.mul_left at succ(cantorPrefix(X, k)), 4 ^ k, 4
        . exact successorBound
      have successorShape : 4 * succ(cantorPrefix(X, k)) =
        4 * cantorPrefix(X, k) + 4
        ring
      rw successorShape at scaledBound
      apply Less.transitive_LessEqual at
        4 * cantorPrefix(X, k) + 2,
        4 * cantorPrefix(X, k) + 4,
        4 * (4 ^ k)
      . typecheck
      . typecheck