Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Mathlib.Data.Nat.Size
public import Mathlib.Tactic.Attr.Core
public import Mathlib.Tactic.Push

set_option doc.verso true

Binary counter costs

Least-significant-bit-first increment changes an initial sequence of ones and the next zero. The number of ones is a potential that bounds the total changes under repeated increments. These are costs of the list algorithm; a Turing-machine bound additionally requires simulation.

Main definitions

increment: binary increment, permitting leading zeroes.
flips: the number of digits changed by an increment.
totalFlips: the cumulative digit changes starting at zero.

Main statements

flips_add_count_increment: the exact potential identity.
totalFlips_le: at most two changes per increment, amortized.
flips_bits_le_succ_size: the incremented number's binary size bounds all changed bits.
size_mono: increasing counter values have nondecreasing binary size.

Tags

binary counter, amortized complexity, potential

@[expose] public sectionnamespace Geb.BitTree.Counter

Increment a binary word whose least significant digit comes first.

def increment : List Bool → List Bool :=
  List.rec [true] fun b bs next ↦ if b then false :: next else true :: bs

Number of bit changes, including the final zero-to-one change.

def flips : List Bool → ℕ :=
  List.foldr (fun b n ↦ if b then n + 1 else 1) 1

Carry propagation resets an initial sequence of ones.

theorem increment_replicate_true_append (k : ℕ) (bs : List Bool) :
    increment (List.replicate k true ++ bs) =
      List.replicate k false ++ increment bs := byk:ℕbs:List Bool⊢ increment (List.replicate k true ++ bs) = List.replicate k false ++ increment bs
  apply Nat.rec (motive := fun k ↦
    increment (List.replicate k true ++ bs) =
      List.replicate k false ++ increment bs) ?_ ?_ kk:ℕbs:List Bool⊢ increment (List.replicate Nat.zero true ++ bs) = List.replicate Nat.zero false ++ increment bsk:ℕbs:List Bool⊢ ∀ (n : ℕ),
  increment (List.replicate n true ++ bs) = List.replicate n false ++ increment bs →
    increment (List.replicate n.succ true ++ bs) = List.replicate n.succ false ++ increment bs
  ·k:ℕbs:List Bool⊢ increment (List.replicate Nat.zero true ++ bs) = List.replicate Nat.zero false ++ increment bs rflAll goals completed! 🐙
  ·k:ℕbs:List Bool⊢ ∀ (n : ℕ),
  increment (List.replicate n true ++ bs) = List.replicate n false ++ increment bs →
    increment (List.replicate n.succ true ++ bs) = List.replicate n.succ false ++ increment bs intro k ihk✝:ℕbs:List Boolk:ℕih:increment (List.replicate k true ++ bs) = List.replicate k false ++ increment bs⊢ increment (List.replicate k.succ true ++ bs) = List.replicate k.succ false ++ increment bs
    simpa [List.replicate_succ, increment] using congrArg (false :: ·) ihAll goals completed! 🐙

Every initial one contributes one bit change before the remaining increment.

theorem flips_replicate_true_append (k : ℕ) (bs : List Bool) :
    flips (List.replicate k true ++ bs) = k + flips bs := byk:ℕbs:List Bool⊢ flips (List.replicate k true ++ bs) = k + flips bs
  apply Nat.rec (motive := fun k ↦
    flips (List.replicate k true ++ bs) = k + flips bs) ?_ ?_ kk:ℕbs:List Bool⊢ flips (List.replicate Nat.zero true ++ bs) = Nat.zero + flips bsk:ℕbs:List Bool⊢ ∀ (n : ℕ),
  flips (List.replicate n true ++ bs) = n + flips bs → flips (List.replicate n.succ true ++ bs) = n.succ + flips bs
  ·k:ℕbs:List Bool⊢ flips (List.replicate Nat.zero true ++ bs) = Nat.zero + flips bs simpAll goals completed! 🐙
  ·k:ℕbs:List Bool⊢ ∀ (n : ℕ),
  flips (List.replicate n true ++ bs) = n + flips bs → flips (List.replicate n.succ true ++ bs) = n.succ + flips bs intro k ihk✝:ℕbs:List Boolk:ℕih:flips (List.replicate k true ++ bs) = k + flips bs⊢ flips (List.replicate k.succ true ++ bs) = k.succ + flips bs
    simp [List.replicate_succ, flips] at ih ⊢k✝:ℕbs:List Boolk:ℕih:List.foldr (fun b n ↦ if b = true then n + 1 else 1) (List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs)
    (List.replicate k true) =
  k + List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs⊢ List.foldr (fun b n ↦ if b = true then n + 1 else 1) (List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs)
      (List.replicate k true) +
    1 =
  k + 1 + List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs
    omegaAll goals completed! 🐙

Every increment changes at least one bit.

theorem flips_pos (bs : List Bool) : 0 < flips bs := bybs:List Bool⊢ 0 < flips bs
  apply List.rec (motive := fun bs ↦ 0 < flips bs) ?_ ?_ bsbs:List Bool⊢ 0 < flips []bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool), 0 < flips tail → 0 < flips (head :: tail)
  ·bs:List Bool⊢ 0 < flips [] decideAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool), 0 < flips tail → 0 < flips (head :: tail) intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:0 < flips bs⊢ 0 < flips (b :: bs)
    cases bfalsebs✝:List Boolbs:List Boolih:0 < flips bs⊢ 0 < flips (false :: bs)truebs✝:List Boolbs:List Boolih:0 < flips bs⊢ 0 < flips (true :: bs) <;>falsebs✝:List Boolbs:List Boolih:0 < flips bs⊢ 0 < flips (false :: bs)truebs✝:List Boolbs:List Boolih:0 < flips bs⊢ 0 < flips (true :: bs) simp_all [flips]All goals completed! 🐙

Every bit strictly before the last changed position is one.

theorem getD_eq_true_of_lt_flips (bs : List Bool) (i : ℕ) (h : i + 1 < flips bs) :
    bs[i]?.getD false = true := bybs:List Booli:ℕh:i + 1 < flips bs⊢ bs[i]?.getD false = true
  revert ibs:List Bool⊢ ∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = true
  apply List.rec (motive := fun bs ↦ ∀ i, i + 1 < flips bs →
    bs[i]?.getD false = true) ?_ ?_ bsbs:List Bool⊢ ∀ (i : ℕ), i + 1 < flips [] → [][i]?.getD false = truebs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ), i + 1 < flips tail → tail[i]?.getD false = true) →
    ∀ (i : ℕ), i + 1 < flips (head :: tail) → (head :: tail)[i]?.getD false = true
  ·bs:List Bool⊢ ∀ (i : ℕ), i + 1 < flips [] → [][i]?.getD false = true intro i hibs:List Booli:ℕhi:i + 1 < flips []⊢ [][i]?.getD false = true
    simp only [flips, List.foldr_nil] at hibs:List Booli:ℕhi:i + 1 < 1⊢ [][i]?.getD false = true
    omegaAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ), i + 1 < flips tail → tail[i]?.getD false = true) →
    ∀ (i : ℕ), i + 1 < flips (head :: tail) → (head :: tail)[i]?.getD false = true intro b bs ih i hibs✝:List Boolb:Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 < flips (b :: bs)⊢ (b :: bs)[i]?.getD false = true
    cases bfalsebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 < flips (false :: bs)⊢ (false :: bs)[i]?.getD false = truetruebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 < flips (true :: bs)⊢ (true :: bs)[i]?.getD false = true
    ·falsebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 < flips (false :: bs)⊢ (false :: bs)[i]?.getD false = true simp only [flips, List.foldr_cons, Bool.false_eq_true, ↓reduceIte] at hifalsebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 < 1⊢ (false :: bs)[i]?.getD false = true
      omegaAll goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 < flips (true :: bs)⊢ (true :: bs)[i]?.getD false = true cases i with
      | zero =>true.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truehi:0 + 1 < flips (true :: bs)⊢ (true :: bs)[0]?.getD false = true rflAll goals completed! 🐙
      | succ i =>true.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 + 1 < flips (true :: bs)⊢ (true :: bs)[i + 1]?.getD false = true
        change bs[i]?.getD false = truetrue.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 + 1 < flips (true :: bs)⊢ bs[i]?.getD false = true
        apply ihtrue.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 + 1 < flips (true :: bs)⊢ i + 1 < flips bs
        change i + 1 + 1 < flips bs + 1 at hitrue.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < flips bs → bs[i]?.getD false = truei:ℕhi:i + 1 + 1 < flips bs + 1⊢ i + 1 < flips bs
        omegaAll goals completed! 🐙

The final changed position contains zero, counting blanks as zero.

theorem getD_last_flip (bs : List Bool) : bs[flips bs - 1]?.getD false = false := bybs:List Bool⊢ bs[flips bs - 1]?.getD false = false
  apply List.rec (motive := fun bs ↦ bs[flips bs - 1]?.getD false = false) ?_ ?_ bsbs:List Bool⊢ [][flips [] - 1]?.getD false = falsebs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  tail[flips tail - 1]?.getD false = false → (head :: tail)[flips (head :: tail) - 1]?.getD false = false
  ·bs:List Bool⊢ [][flips [] - 1]?.getD false = false rflAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  tail[flips tail - 1]?.getD false = false → (head :: tail)[flips (head :: tail) - 1]?.getD false = false intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:bs[flips bs - 1]?.getD false = false⊢ (b :: bs)[flips (b :: bs) - 1]?.getD false = false
    cases bfalsebs✝:List Boolbs:List Boolih:bs[flips bs - 1]?.getD false = false⊢ (false :: bs)[flips (false :: bs) - 1]?.getD false = falsetruebs✝:List Boolbs:List Boolih:bs[flips bs - 1]?.getD false = false⊢ (true :: bs)[flips (true :: bs) - 1]?.getD false = false
    ·falsebs✝:List Boolbs:List Boolih:bs[flips bs - 1]?.getD false = false⊢ (false :: bs)[flips (false :: bs) - 1]?.getD false = false rflAll goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:bs[flips bs - 1]?.getD false = false⊢ (true :: bs)[flips (true :: bs) - 1]?.getD false = false have hf := flips_pos bstruebs✝:List Boolbs:List Boolih:bs[flips bs - 1]?.getD false = falsehf:0 < flips bs⊢ (true :: bs)[flips (true :: bs) - 1]?.getD false = false
      have he : flips (true :: bs) - 1 = (flips bs - 1) + 1 := bybs:List Bool⊢ bs[flips bs - 1]?.getD false = false
        change flips bs + 1 - 1 = flips bs - 1 + 1bs✝:List Boolbs:List Boolih:bs[flips bs - 1]?.getD false = falsehf:0 < flips bs⊢ flips bs + 1 - 1 = flips bs - 1 + 1
        omegatruebs✝:List Boolbs:List Boolih:bs[flips bs - 1]?.getD false = falsehf:0 < flips bshe:flips (true :: bs) - 1 = flips bs - 1 + 1⊢ (true :: bs)[flips (true :: bs) - 1]?.getD false = false
      simpa only [he, List.getElem?_cons_succ] using ihAll goals completed! 🐙

Increment resets the initial ones, sets the following zero, and preserves later bits.

theorem getD_increment (bs : List Bool) (i : ℕ) :
    (increment bs)[i]?.getD false =
      if i + 1 < flips bs then false
      else if i + 1 = flips bs then true else bs[i]?.getD false := bybs:List Booli:ℕ⊢ (increment bs)[i]?.getD false = if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD false
  revert ibs:List Bool⊢ ∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD false
  apply List.rec (motive := fun bs ↦ ∀ i,
    (increment bs)[i]?.getD false =
      if i + 1 < flips bs then false
      else if i + 1 = flips bs then true else bs[i]?.getD false) ?_ ?_ bsbs:List Bool⊢ ∀ (i : ℕ),
  (increment [])[i]?.getD false =
    if i + 1 < flips [] then false else if i + 1 = flips [] then true else [][i]?.getD falsebs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ),
      (increment tail)[i]?.getD false =
        if i + 1 < flips tail then false else if i + 1 = flips tail then true else tail[i]?.getD false) →
    ∀ (i : ℕ),
      (increment (head :: tail))[i]?.getD false =
        if i + 1 < flips (head :: tail) then false
        else if i + 1 = flips (head :: tail) then true else (head :: tail)[i]?.getD false
  ·bs:List Bool⊢ ∀ (i : ℕ),
  (increment [])[i]?.getD false =
    if i + 1 < flips [] then false else if i + 1 = flips [] then true else [][i]?.getD false intro ibs:List Booli:ℕ⊢ (increment [])[i]?.getD false = if i + 1 < flips [] then false else if i + 1 = flips [] then true else [][i]?.getD false
    cases i with
    | zero =>zerobs:List Bool⊢ (increment [])[0]?.getD false = if 0 + 1 < flips [] then false else if 0 + 1 = flips [] then true else [][0]?.getD false rflAll goals completed! 🐙
    | succ i =>succbs:List Booli:ℕ⊢ (increment [])[i + 1]?.getD false =
  if i + 1 + 1 < flips [] then false else if i + 1 + 1 = flips [] then true else [][i + 1]?.getD false
      change false = if i + 1 + 1 < 1 then false
        else if i + 1 + 1 = 1 then true else falsesuccbs:List Booli:ℕ⊢ false = if i + 1 + 1 < 1 then false else if i + 1 + 1 = 1 then true else false
      simp only [show ¬i + 1 + 1 < 1 from by omega,
        show i + 1 + 1 ≠ 1 from by omega, ↓reduceIte]All goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ),
      (increment tail)[i]?.getD false =
        if i + 1 < flips tail then false else if i + 1 = flips tail then true else tail[i]?.getD false) →
    ∀ (i : ℕ),
      (increment (head :: tail))[i]?.getD false =
        if i + 1 < flips (head :: tail) then false
        else if i + 1 = flips (head :: tail) then true else (head :: tail)[i]?.getD false intro b bs ih ibs✝:List Boolb:Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment (b :: bs))[i]?.getD false =
  if i + 1 < flips (b :: bs) then false else if i + 1 = flips (b :: bs) then true else (b :: bs)[i]?.getD false
    cases bfalsebs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment (false :: bs))[i]?.getD false =
  if i + 1 < flips (false :: bs) then false
  else if i + 1 = flips (false :: bs) then true else (false :: bs)[i]?.getD falsetruebs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment (true :: bs))[i]?.getD false =
  if i + 1 < flips (true :: bs) then false else if i + 1 = flips (true :: bs) then true else (true :: bs)[i]?.getD false
    ·falsebs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment (false :: bs))[i]?.getD false =
  if i + 1 < flips (false :: bs) then false
  else if i + 1 = flips (false :: bs) then true else (false :: bs)[i]?.getD false cases i with
      | zero =>false.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD false⊢ (increment (false :: bs))[0]?.getD false =
  if 0 + 1 < flips (false :: bs) then false
  else if 0 + 1 = flips (false :: bs) then true else (false :: bs)[0]?.getD false rflAll goals completed! 🐙
      | succ i =>false.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment (false :: bs))[i + 1]?.getD false =
  if i + 1 + 1 < flips (false :: bs) then false
  else if i + 1 + 1 = flips (false :: bs) then true else (false :: bs)[i + 1]?.getD false
        change bs[i]?.getD false = if i + 1 + 1 < 1 then false
          else if i + 1 + 1 = 1 then true else bs[i]?.getD falsefalse.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ bs[i]?.getD false = if i + 1 + 1 < 1 then false else if i + 1 + 1 = 1 then true else bs[i]?.getD false
        simp only [show ¬i + 1 + 1 < 1 from by omega,
          show i + 1 + 1 ≠ 1 from by omega, ↓reduceIte]All goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment (true :: bs))[i]?.getD false =
  if i + 1 < flips (true :: bs) then false else if i + 1 = flips (true :: bs) then true else (true :: bs)[i]?.getD false cases i with
      | zero =>true.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD false⊢ (increment (true :: bs))[0]?.getD false =
  if 0 + 1 < flips (true :: bs) then false else if 0 + 1 = flips (true :: bs) then true else (true :: bs)[0]?.getD false
        have hf := flips_pos bstrue.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsehf:0 < flips bs⊢ (increment (true :: bs))[0]?.getD false =
  if 0 + 1 < flips (true :: bs) then false else if 0 + 1 = flips (true :: bs) then true else (true :: bs)[0]?.getD false
        change false = if 1 < flips bs + 1 then false
          else if 1 = flips bs + 1 then true else truetrue.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsehf:0 < flips bs⊢ false = if 1 < flips bs + 1 then false else if 1 = flips bs + 1 then true else true
        simp only [show 1 < flips bs + 1 from by omega, ↓reduceIte]All goals completed! 🐙
      | succ i =>true.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment (true :: bs))[i + 1]?.getD false =
  if i + 1 + 1 < flips (true :: bs) then false
  else if i + 1 + 1 = flips (true :: bs) then true else (true :: bs)[i + 1]?.getD false
        change (increment bs)[i]?.getD false =
          if i + 1 + 1 < flips bs + 1 then false
          else if i + 1 + 1 = flips bs + 1 then true else bs[i]?.getD falsetrue.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ (increment bs)[i]?.getD false =
  if i + 1 + 1 < flips bs + 1 then false else if i + 1 + 1 = flips bs + 1 then true else bs[i]?.getD false
        have hlt : (i + 1 + 1 < flips bs + 1) ↔ (i + 1 < flips bs) := bybs:List Booli:ℕ⊢ (increment bs)[i]?.getD false = if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD false
          constructormpbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ i + 1 + 1 < flips bs + 1 → i + 1 < flips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ i + 1 < flips bs → i + 1 + 1 < flips bs + 1 <;>mpbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ i + 1 + 1 < flips bs + 1 → i + 1 < flips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕ⊢ i + 1 < flips bs → i + 1 + 1 < flips bs + 1 intro hmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕh:i + 1 < flips bs⊢ i + 1 + 1 < flips bs + 1 <;>mpbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕh:i + 1 + 1 < flips bs + 1⊢ i + 1 < flips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕh:i + 1 < flips bs⊢ i + 1 + 1 < flips bs + 1 omegatrue.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bs⊢ (increment bs)[i]?.getD false =
  if i + 1 + 1 < flips bs + 1 then false else if i + 1 + 1 = flips bs + 1 then true else bs[i]?.getD false
        have heq : (i + 1 + 1 = flips bs + 1) ↔ (i + 1 = flips bs) := bybs:List Booli:ℕ⊢ (increment bs)[i]?.getD false = if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD false
          constructormpbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bs⊢ i + 1 + 1 = flips bs + 1 → i + 1 = flips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bs⊢ i + 1 = flips bs → i + 1 + 1 = flips bs + 1 <;>mpbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bs⊢ i + 1 + 1 = flips bs + 1 → i + 1 = flips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bs⊢ i + 1 = flips bs → i + 1 + 1 = flips bs + 1 intro hmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bsh:i + 1 = flips bs⊢ i + 1 + 1 = flips bs + 1 <;>mpbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bsh:i + 1 + 1 = flips bs + 1⊢ i + 1 = flips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bsh:i + 1 = flips bs⊢ i + 1 + 1 = flips bs + 1 omegatrue.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ),
  (increment bs)[i]?.getD false =
    if i + 1 < flips bs then false else if i + 1 = flips bs then true else bs[i]?.getD falsei:ℕhlt:i + 1 + 1 < flips bs + 1 ↔ i + 1 < flips bsheq:i + 1 + 1 = flips bs + 1 ↔ i + 1 = flips bs⊢ (increment bs)[i]?.getD false =
  if i + 1 + 1 < flips bs + 1 then false else if i + 1 + 1 = flips bs + 1 then true else bs[i]?.getD false
        simpa only [hlt, heq] using ih iAll goals completed! 🐙

Each increment consumes one unit of potential for every trailing one it resets.

theorem flips_add_count_increment (bs : List Bool) :
    flips bs + (increment bs).count true = bs.count true + 2 := bybs:List Bool⊢ flips bs + List.count true (increment bs) = List.count true bs + 2
  apply List.rec (motive := fun bs ↦
    flips bs + (increment bs).count true = bs.count true + 2) ?_ ?_ bsbs:List Bool⊢ flips [] + List.count true (increment []) = List.count true [] + 2bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  flips tail + List.count true (increment tail) = List.count true tail + 2 →
    flips (head :: tail) + List.count true (increment (head :: tail)) = List.count true (head :: tail) + 2
  ·bs:List Bool⊢ flips [] + List.count true (increment []) = List.count true [] + 2 rflAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  flips tail + List.count true (increment tail) = List.count true tail + 2 →
    flips (head :: tail) + List.count true (increment (head :: tail)) = List.count true (head :: tail) + 2 intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:flips bs + List.count true (increment bs) = List.count true bs + 2⊢ flips (b :: bs) + List.count true (increment (b :: bs)) = List.count true (b :: bs) + 2
    cases bfalsebs✝:List Boolbs:List Boolih:flips bs + List.count true (increment bs) = List.count true bs + 2⊢ flips (false :: bs) + List.count true (increment (false :: bs)) = List.count true (false :: bs) + 2truebs✝:List Boolbs:List Boolih:flips bs + List.count true (increment bs) = List.count true bs + 2⊢ flips (true :: bs) + List.count true (increment (true :: bs)) = List.count true (true :: bs) + 2 <;>falsebs✝:List Boolbs:List Boolih:flips bs + List.count true (increment bs) = List.count true bs + 2⊢ flips (false :: bs) + List.count true (increment (false :: bs)) = List.count true (false :: bs) + 2truebs✝:List Boolbs:List Boolih:flips bs + List.count true (increment bs) = List.count true bs + 2⊢ flips (true :: bs) + List.count true (increment (true :: bs)) = List.count true (true :: bs) + 2 simp_all [flips, increment]truebs✝:List Boolbs:List Boolih:List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs +
    List.count true (List.rec [true] (fun b bs next ↦ if b = true then false :: next else true :: bs) bs) =
  List.count true bs + 2⊢ List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs + 1 +
    List.count true (List.rec [true] (fun b bs next ↦ if b = true then false :: next else true :: bs) bs) =
  List.count true bs + 1 + 2 <;>falsebs✝:List Boolbs:List Boolih:List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs +
    List.count true (List.rec [true] (fun b bs next ↦ if b = true then false :: next else true :: bs) bs) =
  List.count true bs + 2⊢ 1 + (List.count true bs + 1) = List.count true bs + 2truebs✝:List Boolbs:List Boolih:List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs +
    List.count true (List.rec [true] (fun b bs next ↦ if b = true then false :: next else true :: bs) bs) =
  List.count true bs + 2⊢ List.foldr (fun b n ↦ if b = true then n + 1 else 1) 1 bs + 1 +
    List.count true (List.rec [true] (fun b bs next ↦ if b = true then false :: next else true :: bs) bs) =
  List.count true bs + 1 + 2 omegaAll goals completed! 🐙

Binary increment agrees with successor on natural numbers.

theorem increment_bits (n : ℕ) : increment n.bits = (n + 1).bits := byn:ℕ⊢ increment n.bits = (n + 1).bits
  apply Nat.binaryRec' (motive := fun n ↦ increment n.bits = (n + 1).bits) ?_ ?_ nn:ℕ⊢ increment (Nat.bits 0) = (0 + 1).bitsn:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) → increment n.bits = (n + 1).bits → increment (Nat.bit b n).bits = (Nat.bit b n + 1).bits
  ·n:ℕ⊢ increment (Nat.bits 0) = (0 + 1).bits rflAll goals completed! 🐙
  ·n:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) → increment n.bits = (n + 1).bits → increment (Nat.bit b n).bits = (Nat.bit b n + 1).bits intro b k hk ihn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:increment k.bits = (k + 1).bits⊢ increment (Nat.bit b k).bits = (Nat.bit b k + 1).bits
    rw [Nat.bits_append_bit k b hkn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:increment k.bits = (k + 1).bits⊢ increment (b :: k.bits) = (Nat.bit b k + 1).bits]n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:increment k.bits = (k + 1).bits⊢ increment (b :: k.bits) = (Nat.bit b k + 1).bits
    cases bfalsen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → false = true⊢ increment (false :: k.bits) = (Nat.bit false k + 1).bitstruen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = true⊢ increment (true :: k.bits) = (Nat.bit true k + 1).bits
    ·falsen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → false = true⊢ increment (false :: k.bits) = (Nat.bit false k + 1).bits simp [increment, Nat.bit_val, Nat.bit1_bits]All goals completed! 🐙
    ·truen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = true⊢ increment (true :: k.bits) = (Nat.bit true k + 1).bits change false :: increment k.bits = (Nat.bit true k + 1).bitstruen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = true⊢ false :: increment k.bits = (Nat.bit true k + 1).bits
      rw [ih,truen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = true⊢ false :: (k + 1).bits = (Nat.bit true k + 1).bits Nat.bit_valtruen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = true⊢ false :: (k + 1).bits = (2 * k + true.toNat + 1).bits]truen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = true⊢ false :: (k + 1).bits = (2 * k + true.toNat + 1).bits
      have he : 2 * k + true.toNat + 1 = 2 * (k + 1) := byn:ℕ⊢ increment n.bits = (n + 1).bits simpn:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = true⊢ 2 * k + 1 + 1 = 2 * (k + 1); omegatruen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = truehe:2 * k + true.toNat + 1 = 2 * (k + 1)⊢ false :: (k + 1).bits = (2 * k + true.toNat + 1).bits
      rw [he,truen:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = truehe:2 * k + true.toNat + 1 = 2 * (k + 1)⊢ false :: (k + 1).bits = (2 * (k + 1)).bits Nat.bit0_bits (k + 1) (byn:ℕk:ℕih:increment k.bits = (k + 1).bitshk:k = 0 → true = truehe:2 * k + true.toNat + 1 = 2 * (k + 1)⊢ k + 1 ≠ 0 omegaAll goals completed! 🐙)]All goals completed! 🐙

Cumulative bit changes of increments from zero to the argument.

def totalFlips : ℕ → ℕ :=
  Nat.rec 0 fun n cost ↦ cost + flips n.bits

Total changes plus the final potential equal twice the number of increments.

theorem totalFlips_add_count (n : ℕ) : totalFlips n + n.bits.count true = 2 * n := byn:ℕ⊢ totalFlips n + List.count true n.bits = 2 * n
  apply Nat.rec (motive := fun n ↦ totalFlips n + n.bits.count true = 2 * n) ?_ ?_ nn:ℕ⊢ totalFlips Nat.zero + List.count true Nat.zero.bits = 2 * Nat.zeron:ℕ⊢ ∀ (n : ℕ), totalFlips n + List.count true n.bits = 2 * n → totalFlips n.succ + List.count true n.succ.bits = 2 * n.succ
  ·n:ℕ⊢ totalFlips Nat.zero + List.count true Nat.zero.bits = 2 * Nat.zero rflAll goals completed! 🐙
  ·n:ℕ⊢ ∀ (n : ℕ), totalFlips n + List.count true n.bits = 2 * n → totalFlips n.succ + List.count true n.succ.bits = 2 * n.succ intro k ihn:ℕk:ℕih:totalFlips k + List.count true k.bits = 2 * k⊢ totalFlips k.succ + List.count true k.succ.bits = 2 * k.succ
    have h := flips_add_count_increment k.bitsn:ℕk:ℕih:totalFlips k + List.count true k.bits = 2 * kh:flips k.bits + List.count true (increment k.bits) = List.count true k.bits + 2⊢ totalFlips k.succ + List.count true k.succ.bits = 2 * k.succ
    rw [increment_bitsn:ℕk:ℕih:totalFlips k + List.count true k.bits = 2 * kh:flips k.bits + List.count true (k + 1).bits = List.count true k.bits + 2⊢ totalFlips k.succ + List.count true k.succ.bits = 2 * k.succ] at hn:ℕk:ℕih:totalFlips k + List.count true k.bits = 2 * kh:flips k.bits + List.count true (k + 1).bits = List.count true k.bits + 2⊢ totalFlips k.succ + List.count true k.succ.bits = 2 * k.succ
    change totalFlips k + flips k.bits + (k + 1).bits.count true = 2 * (k + 1)n:ℕk:ℕih:totalFlips k + List.count true k.bits = 2 * kh:flips k.bits + List.count true (k + 1).bits = List.count true k.bits + 2⊢ totalFlips k + flips k.bits + List.count true (k + 1).bits = 2 * (k + 1)
    omegaAll goals completed! 🐙

Binary increment changes at most two digits per increment, amortized.

theorem totalFlips_le (n : ℕ) : totalFlips n ≤ 2 * n := byn:ℕ⊢ totalFlips n ≤ 2 * n
  have h := totalFlips_add_count nn:ℕh:totalFlips n + List.count true n.bits = 2 * n⊢ totalFlips n ≤ 2 * n
  omegaAll goals completed! 🐙

An increment visits no more than the represented digits and the first blank digit.

theorem flips_le_length (bs : List Bool) : flips bs ≤ bs.length + 1 := bybs:List Bool⊢ flips bs ≤ bs.length + 1
  apply List.rec (motive := fun bs ↦ flips bs ≤ bs.length + 1) ?_ ?_ bsbs:List Bool⊢ flips [] ≤ [].length + 1bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool), flips tail ≤ tail.length + 1 → flips (head :: tail) ≤ (head :: tail).length + 1
  ·bs:List Bool⊢ flips [] ≤ [].length + 1 exact Nat.le_refl _All goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool), flips tail ≤ tail.length + 1 → flips (head :: tail) ≤ (head :: tail).length + 1 intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:flips bs ≤ bs.length + 1⊢ flips (b :: bs) ≤ (b :: bs).length + 1
    cases bfalsebs✝:List Boolbs:List Boolih:flips bs ≤ bs.length + 1⊢ flips (false :: bs) ≤ (false :: bs).length + 1truebs✝:List Boolbs:List Boolih:flips bs ≤ bs.length + 1⊢ flips (true :: bs) ≤ (true :: bs).length + 1 <;>falsebs✝:List Boolbs:List Boolih:flips bs ≤ bs.length + 1⊢ flips (false :: bs) ≤ (false :: bs).length + 1truebs✝:List Boolbs:List Boolih:flips bs ≤ bs.length + 1⊢ flips (true :: bs) ≤ (true :: bs).length + 1 simp_all [flips]All goals completed! 🐙

Every changed digit belongs to the resulting counter representation.

theorem flips_le_increment_length (bs : List Bool) : flips bs ≤ (increment bs).length := bybs:List Bool⊢ flips bs ≤ (increment bs).length
  apply List.rec (motive := fun bs ↦ flips bs ≤ (increment bs).length) ?_ ?_ bsbs:List Bool⊢ flips [] ≤ (increment []).lengthbs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  flips tail ≤ (increment tail).length → flips (head :: tail) ≤ (increment (head :: tail)).length
  ·bs:List Bool⊢ flips [] ≤ (increment []).length exact Nat.le_refl _All goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  flips tail ≤ (increment tail).length → flips (head :: tail) ≤ (increment (head :: tail)).length intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:flips bs ≤ (increment bs).length⊢ flips (b :: bs) ≤ (increment (b :: bs)).length
    cases bfalsebs✝:List Boolbs:List Boolih:flips bs ≤ (increment bs).length⊢ flips (false :: bs) ≤ (increment (false :: bs)).lengthtruebs✝:List Boolbs:List Boolih:flips bs ≤ (increment bs).length⊢ flips (true :: bs) ≤ (increment (true :: bs)).length <;>falsebs✝:List Boolbs:List Boolih:flips bs ≤ (increment bs).length⊢ flips (false :: bs) ≤ (increment (false :: bs)).lengthtruebs✝:List Boolbs:List Boolih:flips bs ≤ (increment bs).length⊢ flips (true :: bs) ≤ (increment (true :: bs)).length simp_all [flips, increment]All goals completed! 🐙

The incremented number's binary size bounds all digits changed by the increment.

theorem flips_bits_le_succ_size (n : ℕ) : flips n.bits ≤ (n + 1).size := byn:ℕ⊢ flips n.bits ≤ (n + 1).size
  have h := flips_le_increment_length n.bitsn:ℕh:flips n.bits ≤ (increment n.bits).length⊢ flips n.bits ≤ (n + 1).size
  rwa [increment_bits,n:ℕh:flips n.bits ≤ (n + 1).bits.length⊢ flips n.bits ≤ (n + 1).size Nat.size_eq_bits_lenn:ℕh:flips n.bits ≤ (n + 1).size⊢ flips n.bits ≤ (n + 1).size]n:ℕh:flips n.bits ≤ (n + 1).size⊢ flips n.bits ≤ (n + 1).size at h

A counter value has exactly its binary size in represented digits.

theorem length_bits (n : ℕ) : n.bits.length = n.size := Nat.size_eq_bits_len n

An increment visits at most one more cell than the binary size of its argument.

theorem flips_bits_le (n : ℕ) : flips n.bits ≤ n.size + 1 := byn:ℕ⊢ flips n.bits ≤ n.size + 1
  simpa [length_bits] using flips_le_length n.bitsAll goals completed! 🐙

A number below a power of two uses no more digits than that exponent.

theorem size_le_of_lt_pow (n w : ℕ) (h : n < 2 ^ w) : n.size ≤ w := byn:ℕw:ℕh:n < 2 ^ w⊢ n.size ≤ w
  revert wn:ℕ⊢ ∀ (w : ℕ), n < 2 ^ w → n.size ≤ w
  apply Nat.binaryRec' (motive := fun n ↦ ∀ w, n < 2 ^ w → n.size ≤ w) ?_ ?_ nn:ℕ⊢ ∀ (w : ℕ), 0 < 2 ^ w → Nat.size 0 ≤ wn:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) → (∀ (w : ℕ), n < 2 ^ w → n.size ≤ w) → ∀ (w : ℕ), Nat.bit b n < 2 ^ w → (Nat.bit b n).size ≤ w
  ·n:ℕ⊢ ∀ (w : ℕ), 0 < 2 ^ w → Nat.size 0 ≤ w intro w _n:ℕw:ℕa✝:0 < 2 ^ w⊢ Nat.size 0 ≤ w
    simpAll goals completed! 🐙
  ·n:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) → (∀ (w : ℕ), n < 2 ^ w → n.size ≤ w) → ∀ (w : ℕ), Nat.bit b n < 2 ^ w → (Nat.bit b n).size ≤ w intro b k hk ih w hn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕh:Nat.bit b k < 2 ^ w⊢ (Nat.bit b k).size ≤ w
    have hn : Nat.bit b k ≠ 0 := byn:ℕw:ℕh:n < 2 ^ w⊢ n.size ≤ w
      cases bfalsen:ℕk:ℕih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕhk:k = 0 → false = trueh:Nat.bit false k < 2 ^ w⊢ Nat.bit false k ≠ 0truen:ℕk:ℕih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕhk:k = 0 → true = trueh:Nat.bit true k < 2 ^ w⊢ Nat.bit true k ≠ 0 <;>falsen:ℕk:ℕih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕhk:k = 0 → false = trueh:Nat.bit false k < 2 ^ w⊢ Nat.bit false k ≠ 0truen:ℕk:ℕih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕhk:k = 0 → true = trueh:Nat.bit true k < 2 ^ w⊢ Nat.bit true k ≠ 0 simp_all [Nat.bit_val]All goals completed! 🐙
      omegan:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕh:Nat.bit b k < 2 ^ whn:Nat.bit b k ≠ 0⊢ (Nat.bit b k).size ≤ w
    rw [Nat.size_bit hnn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕh:Nat.bit b k < 2 ^ whn:Nat.bit b k ≠ 0⊢ k.size.succ ≤ w]n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ ww:ℕh:Nat.bit b k < 2 ^ whn:Nat.bit b k ≠ 0⊢ k.size.succ ≤ w
    cases w with
    | zero =>zeron:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0h:Nat.bit b k < 2 ^ 0⊢ k.size.succ ≤ 0 simp only [Nat.pow_zero] at hzeron:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0h:Nat.bit b k < 1⊢ k.size.succ ≤ 0; omegaAll goals completed! 🐙
    | succ w =>succn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0w:ℕh:Nat.bit b k < 2 ^ (w + 1)⊢ k.size.succ ≤ w + 1
      have hk' : k < 2 ^ w := byn:ℕw:ℕh:n < 2 ^ w⊢ n.size ≤ w
        rw [Nat.bit_val,n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0w:ℕh:2 * k + b.toNat < 2 ^ (w + 1)⊢ k < 2 ^ w Nat.pow_succn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0w:ℕh:2 * k + b.toNat < 2 ^ w * 2⊢ k < 2 ^ w] at hn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0w:ℕh:2 * k + b.toNat < 2 ^ w * 2⊢ k < 2 ^ w
        omegasuccn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0w:ℕh:Nat.bit b k < 2 ^ (w + 1)hk':k < 2 ^ w⊢ k.size.succ ≤ w + 1
      have hs := ih w hk'succn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:∀ (w : ℕ), k < 2 ^ w → k.size ≤ whn:Nat.bit b k ≠ 0w:ℕh:Nat.bit b k < 2 ^ (w + 1)hk':k < 2 ^ whs:k.size ≤ w⊢ k.size.succ ≤ w + 1
      omegaAll goals completed! 🐙

A number is smaller than the power of two above all its represented digits.

theorem lt_pow_size (n : ℕ) : n < 2 ^ n.size := byn:ℕ⊢ n < 2 ^ n.size
  apply Nat.binaryRec' (motive := fun n ↦ n < 2 ^ n.size) ?_ ?_ nn:ℕ⊢ 0 < 2 ^ Nat.size 0n:ℕ⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → n < 2 ^ n.size → Nat.bit b n < 2 ^ (Nat.bit b n).size
  ·n:ℕ⊢ 0 < 2 ^ Nat.size 0 decideAll goals completed! 🐙
  ·n:ℕ⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → n < 2 ^ n.size → Nat.bit b n < 2 ^ (Nat.bit b n).size intro b k hk ihn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k < 2 ^ k.size⊢ Nat.bit b k < 2 ^ (Nat.bit b k).size
    have hn : Nat.bit b k ≠ 0 := byn:ℕ⊢ n < 2 ^ n.size
      cases bfalsen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → false = true⊢ Nat.bit false k ≠ 0truen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → true = true⊢ Nat.bit true k ≠ 0 <;>falsen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → false = true⊢ Nat.bit false k ≠ 0truen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → true = true⊢ Nat.bit true k ≠ 0 simp_all [Nat.bit_val]All goals completed! 🐙
      omegan:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k < 2 ^ k.sizehn:Nat.bit b k ≠ 0⊢ Nat.bit b k < 2 ^ (Nat.bit b k).size
    rw [Nat.size_bit hn,n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k < 2 ^ k.sizehn:Nat.bit b k ≠ 0⊢ Nat.bit b k < 2 ^ k.size.succ Nat.pow_succ,n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k < 2 ^ k.sizehn:Nat.bit b k ≠ 0⊢ Nat.bit b k < 2 ^ k.size * 2 Nat.bit_valn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k < 2 ^ k.sizehn:Nat.bit b k ≠ 0⊢ 2 * k + b.toNat < 2 ^ k.size * 2]n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k < 2 ^ k.sizehn:Nat.bit b k ≠ 0⊢ 2 * k + b.toNat < 2 ^ k.size * 2
    cases bfalsen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → false = truehn:Nat.bit false k ≠ 0⊢ 2 * k + false.toNat < 2 ^ k.size * 2truen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → true = truehn:Nat.bit true k ≠ 0⊢ 2 * k + true.toNat < 2 ^ k.size * 2 <;>falsen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → false = truehn:Nat.bit false k ≠ 0⊢ 2 * k + false.toNat < 2 ^ k.size * 2truen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → true = truehn:Nat.bit true k ≠ 0⊢ 2 * k + true.toNat < 2 ^ k.size * 2 simp only [Bool.toNat_false, Bool.toNat_true]truen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → true = truehn:Nat.bit true k ≠ 0⊢ 2 * k + 1 < 2 ^ k.size * 2 <;>falsen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → false = truehn:Nat.bit false k ≠ 0⊢ 2 * k + 0 < 2 ^ k.size * 2truen:ℕk:ℕih:k < 2 ^ k.sizehk:k = 0 → true = truehn:Nat.bit true k ≠ 0⊢ 2 * k + 1 < 2 ^ k.size * 2 omegaAll goals completed! 🐙

Binary size is monotone in the represented natural number.

theorem size_mono {m n : ℕ} (h : m ≤ n) : m.size ≤ n.size := bym:ℕn:ℕh:m ≤ n⊢ m.size ≤ n.size
  have hn := lt_pow_size nm:ℕn:ℕh:m ≤ nhn:n < 2 ^ n.size⊢ m.size ≤ n.size
  exact size_le_of_lt_pow m n.size (bym:ℕn:ℕh:m ≤ nhn:n < 2 ^ n.size⊢ m < 2 ^ n.size omegaAll goals completed! 🐙)

end Geb.BitTree.Counter