1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. BinaryMachine
  6. Accounting
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 Geb.Prototypes.Computability.BitTree.Scanner public import Geb.Prototypes.Computability.BitTree.Counter public import Mathlib.Tactic.SplitIfs
set_option doc.verso true

Two monotone counters for the tree scanner

The pending count is the difference between one plus the forks and the completed leaves. Each counter only increases, so binary-counter amortization bounds the combined update cost.

Main definitions

  • Account retains the scanner mode and both monotone counters.

  • account processes an input prefix.

  • runCost sums the costs of the binary-counter macros.

Main statements

  • account_project identifies the accounting state with the pure scanner.

  • runCost_identity expresses the exact amortized cost.

  • runCost_le gives a linear bound.

Tags

binary counter, recognizer, amortized complexity

@[expose] public sectionnamespace Geb.BitTree.BinaryMachine

The finite control and the two monotone counts whose difference is pending work.

The scanner mode.

One plus the number of forks.

The number of completed leaves.

@[ext] structure Account where mode : Mode forks : ℕ leaves : ℕ deriving DecidableEq, Repr

Recover the scanner's pending count by subtraction.

def accountProject (s : Account) : State := (s.mode, s.forks - s.leaves)

The initial account reserves one root and has completed no leaves.

def initialAccount : Account := ⟨.tree, 1, 0⟩

Consume a bit, increasing exactly the counter specified by its mode.

def accountStep (s : Account) (b : Bool) : Account := ⟨(Geb.BitTree.step (accountProject s) b).1, if s.mode = .tree ∧ b = true then s.forks + 1 else s.forks, if s.mode = .string ∧ b = false then s.leaves + 1 else s.leaves⟩

Accounting after an input prefix.

def account (w : List Bool) : Account := w.foldl accountStep initialAccount

A valid account has ordered counts, with equality exactly in terminal modes.

def AccountValid (s : Account) : Prop := s.leaves ≤ s.forks ∧ 0 < s.forks ∧ match s.mode with | .tree | .string | .bit => s.leaves < s.forks | .done | .dead => s.leaves = s.forks

Counter updates preserve the accounting invariant.

theorem accountStep_valid (s : Account) (b : Bool) (h : AccountValid s) : AccountValid (accountStep s b) := s:Accountb:Boolh:AccountValid s⊢ AccountValid (accountStep s b) b:Boolm:Modea:ℕc:ℕh:AccountValid { mode := m, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := m, forks := a, leaves := c } b) b:Boola:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.tree, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.string, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.bit, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.done, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.dead, forks := a, leaves := c } b) b:Boola:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.tree, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.string, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.bit, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.done, forks := a, leaves := c } b)b:Boola:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.dead, forks := a, leaves := c } b) a:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.dead, forks := a, leaves := c } false)a:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.dead, forks := a, leaves := c } true) a:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.tree, forks := a, leaves := c } false)a:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.tree, forks := a, leaves := c } true)a:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.string, forks := a, leaves := c } false)a:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.string, forks := a, leaves := c } true)a:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.bit, forks := a, leaves := c } false)a:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.bit, forks := a, leaves := c } true)a:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.done, forks := a, leaves := c } false)a:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.done, forks := a, leaves := c } true)a:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.dead, forks := a, leaves := c } false)a:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ AccountValid (accountStep { mode := Mode.dead, forks := a, leaves := c } true) a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c = a⊢ c ≤ a ∧ 0 < a ∧ c = a all_goals a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c = ahe:a - c = 1⊢ c ≤ a ∧ 0 < a ∧ c = aa:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c = ahe:¬a - c = 1⊢ c ≤ a ∧ 0 < a ∧ c = a all_goals (try a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c = ahe:¬a - c = 1⊢ c ≤ a ∧ 0 < a ∧ c = a) all_goals exact ⟨a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c = ahe:¬a - c = 1⊢ c ≤ a All goals completed! 🐙, a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c = ahe:¬a - c = 1⊢ 0 < a All goals completed! 🐙, a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c = ahe:¬a - c = 1⊢ c = a All goals completed! 🐙⟩

Projecting one update agrees with the original scanner step.

theorem accountStep_project (s : Account) (b : Bool) (h : AccountValid s) : accountProject (accountStep s b) = Geb.BitTree.step (accountProject s) b := s:Accountb:Boolh:AccountValid s⊢ accountProject (accountStep s b) = step (accountProject s) b b:Boolm:Modea:ℕc:ℕh:AccountValid { mode := m, forks := a, leaves := c }⊢ accountProject (accountStep { mode := m, forks := a, leaves := c } b) = step (accountProject { mode := m, forks := a, leaves := c }) b b:Boola:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.tree, forks := a, leaves := c } b) = step (accountProject { mode := Mode.tree, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.string, forks := a, leaves := c } b) = step (accountProject { mode := Mode.string, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.bit, forks := a, leaves := c } b) = step (accountProject { mode := Mode.bit, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.done, forks := a, leaves := c } b) = step (accountProject { mode := Mode.done, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.dead, forks := a, leaves := c } b) = step (accountProject { mode := Mode.dead, forks := a, leaves := c }) b b:Boola:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.tree, forks := a, leaves := c } b) = step (accountProject { mode := Mode.tree, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.string, forks := a, leaves := c } b) = step (accountProject { mode := Mode.string, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.bit, forks := a, leaves := c } b) = step (accountProject { mode := Mode.bit, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.done, forks := a, leaves := c } b) = step (accountProject { mode := Mode.done, forks := a, leaves := c }) bb:Boola:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.dead, forks := a, leaves := c } b) = step (accountProject { mode := Mode.dead, forks := a, leaves := c }) b a:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.dead, forks := a, leaves := c } false) = step (accountProject { mode := Mode.dead, forks := a, leaves := c }) falsea:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.dead, forks := a, leaves := c } true) = step (accountProject { mode := Mode.dead, forks := a, leaves := c }) true a:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.tree, forks := a, leaves := c } false) = step (accountProject { mode := Mode.tree, forks := a, leaves := c }) falsea:ℕc:ℕh:AccountValid { mode := Mode.tree, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.tree, forks := a, leaves := c } true) = step (accountProject { mode := Mode.tree, forks := a, leaves := c }) truea:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.string, forks := a, leaves := c } false) = step (accountProject { mode := Mode.string, forks := a, leaves := c }) falsea:ℕc:ℕh:AccountValid { mode := Mode.string, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.string, forks := a, leaves := c } true) = step (accountProject { mode := Mode.string, forks := a, leaves := c }) truea:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.bit, forks := a, leaves := c } false) = step (accountProject { mode := Mode.bit, forks := a, leaves := c }) falsea:ℕc:ℕh:AccountValid { mode := Mode.bit, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.bit, forks := a, leaves := c } true) = step (accountProject { mode := Mode.bit, forks := a, leaves := c }) truea:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.done, forks := a, leaves := c } false) = step (accountProject { mode := Mode.done, forks := a, leaves := c }) falsea:ℕc:ℕh:AccountValid { mode := Mode.done, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.done, forks := a, leaves := c } true) = step (accountProject { mode := Mode.done, forks := a, leaves := c }) truea:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.dead, forks := a, leaves := c } false) = step (accountProject { mode := Mode.dead, forks := a, leaves := c }) falsea:ℕc:ℕh:AccountValid { mode := Mode.dead, forks := a, leaves := c }⊢ accountProject (accountStep { mode := Mode.dead, forks := a, leaves := c } true) = step (accountProject { mode := Mode.dead, forks := a, leaves := c }) true All goals completed! 🐙 all_goals first | (a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < a⊢ a - (c + 1) = (Decidable.rec (fun h ↦ (fun x ↦ (Mode.tree, a - c - 1)) h) (fun h ↦ (fun x ↦ (Mode.done, 0)) h) (instDecidableEqNat (accountProject { mode := Mode.string, forks := a, leaves := c }).snd 1)).snd; All goals completed! 🐙) | (a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < ah✝:a - c = 1⊢ ((if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1)).fst, a - (c + 1)) = if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1)a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < ah✝:¬a - c = 1⊢ ((if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1)).fst, a - (c + 1)) = if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1) a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < ah✝:a - c = 1⊢ ((if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1)).fst, a - (c + 1)) = if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1)a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < ah✝:¬a - c = 1⊢ ((if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1)).fst, a - (c + 1)) = if a - c = 1 then (Mode.done, 0) else (Mode.tree, a - c - 1) a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < ah✝:¬a - c = 1⊢ a - (c + 1) = a - c - 1 a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < ah✝:a - c = 1⊢ a - (c + 1) = 0a:ℕc:ℕh:c ≤ a ∧ 0 < a ∧ c < ah✝:¬a - c = 1⊢ a - (c + 1) = a - c - 1 All goals completed! 🐙)

Folding counter updates preserves the invariant.

theorem account_foldl_valid (w : List Bool) : ∀ s, AccountValid s → AccountValid (w.foldl accountStep s) := List.rec (fun _ h ↦ h) (fun b _ ih s h ↦ ih (accountStep s b) (accountStep_valid s b h)) w

Folding commutes with projection to the pure scanner.

theorem account_foldl_project (w : List Bool) : ∀ s, AccountValid s → accountProject (w.foldl accountStep s) = w.foldl Geb.BitTree.step (accountProject s) := List.rec (fun _ _ ↦ rfl) (fun b _ ih s h ↦ w:List Boolb:Boolx✝:List Boolih:∀ (s : Account), AccountValid s → accountProject (List.foldl accountStep s x✝) = List.foldl step (accountProject s) x✝s:Accounth:AccountValid s⊢ accountProject (List.foldl accountStep s (b :: x✝)) = List.foldl step (accountProject s) (b :: x✝) All goals completed! 🐙) w

Every reachable account satisfies the invariant.

theorem account_valid (w : List Bool) : AccountValid (account w) := account_foldl_valid w initialAccount (w:List Bool⊢ AccountValid initialAccount All goals completed! 🐙)

Completed leaves never exceed available tree positions.

theorem account_leaves_le (w : List Bool) : (account w).leaves ≤ (account w).forks := (account_valid w).1

The initial root contributes at least one to the fork counter.

theorem account_forks_pos (w : List Bool) : 0 < (account w).forks := (account_valid w).2.1

Active modes retain a strict excess of tree positions over completed leaves.

theorem account_active_lt (w : List Bool) (h : (account w).mode = .tree ∨ (account w).mode = .string ∨ (account w).mode = .bit) : (account w).leaves < (account w).forks := w:List Boolh:(account w).mode = Mode.tree ∨ (account w).mode = Mode.string ∨ (account w).mode = Mode.bit⊢ (account w).leaves < (account w).forks w:List Boolh:(account w).mode = Mode.tree ∨ (account w).mode = Mode.string ∨ (account w).mode = Mode.bithv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forks⊢ (account w).leaves < (account w).forks w:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.tree⊢ (account w).leaves < (account w).forksw:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.string⊢ (account w).leaves < (account w).forksw:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.bit⊢ (account w).leaves < (account w).forks w:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.tree⊢ (account w).leaves < (account w).forksw:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.string⊢ (account w).leaves < (account w).forksw:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.bit⊢ (account w).leaves < (account w).forks All goals completed! 🐙

Terminal modes have completed all available tree positions.

theorem account_terminal_eq (w : List Bool) (h : (account w).mode = .done ∨ (account w).mode = .dead) : (account w).leaves = (account w).forks := w:List Boolh:(account w).mode = Mode.done ∨ (account w).mode = Mode.dead⊢ (account w).leaves = (account w).forks w:List Boolh:(account w).mode = Mode.done ∨ (account w).mode = Mode.deadhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forks⊢ (account w).leaves = (account w).forks w:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.done⊢ (account w).leaves = (account w).forksw:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.dead⊢ (account w).leaves = (account w).forks w:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.done⊢ (account w).leaves = (account w).forksw:List Boolhv:match (account w).mode with | Mode.tree => (account w).leaves < (account w).forks | Mode.string => (account w).leaves < (account w).forks | Mode.bit => (account w).leaves < (account w).forks | Mode.done => (account w).leaves = (account w).forks | Mode.dead => (account w).leaves = (account w).forksh:(account w).mode = Mode.dead⊢ (account w).leaves = (account w).forks All goals completed! 🐙

The two-counter account projects to the original scanner.

theorem account_project (w : List Bool) : accountProject (account w) = scan w := account_foldl_project w initialAccount (w:List Bool⊢ AccountValid initialAccount All goals completed! 🐙)

A prefix extended by one bit performs one accounting update.

theorem account_append (w : List Bool) (b : Bool) : account (w ++ [b]) = accountStep (account w) b := w:List Boolb:Bool⊢ account (w ++ [b]) = accountStep (account w) b All goals completed! 🐙

One bit increases the sum of counts by at most one.

theorem accountStep_sum_le (s : Account) (b : Bool) : (accountStep s b).forks + (accountStep s b).leaves ≤ s.forks + s.leaves + 1 := s:Accountb:Bool⊢ (accountStep s b).forks + (accountStep s b).leaves ≤ s.forks + s.leaves + 1 b:Boolm:Modea:ℕc:ℕ⊢ (accountStep { mode := m, forks := a, leaves := c } b).forks + (accountStep { mode := m, forks := a, leaves := c } b).leaves ≤ { mode := m, forks := a, leaves := c }.forks + { mode := m, forks := a, leaves := c }.leaves + 1 b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.tree, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.tree, forks := a, leaves := c } b).leaves ≤ { mode := Mode.tree, forks := a, leaves := c }.forks + { mode := Mode.tree, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.string, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.string, forks := a, leaves := c } b).leaves ≤ { mode := Mode.string, forks := a, leaves := c }.forks + { mode := Mode.string, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.bit, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.bit, forks := a, leaves := c } b).leaves ≤ { mode := Mode.bit, forks := a, leaves := c }.forks + { mode := Mode.bit, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.done, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.done, forks := a, leaves := c } b).leaves ≤ { mode := Mode.done, forks := a, leaves := c }.forks + { mode := Mode.done, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.dead, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.dead, forks := a, leaves := c } b).leaves ≤ { mode := Mode.dead, forks := a, leaves := c }.forks + { mode := Mode.dead, forks := a, leaves := c }.leaves + 1 b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.tree, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.tree, forks := a, leaves := c } b).leaves ≤ { mode := Mode.tree, forks := a, leaves := c }.forks + { mode := Mode.tree, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.string, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.string, forks := a, leaves := c } b).leaves ≤ { mode := Mode.string, forks := a, leaves := c }.forks + { mode := Mode.string, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.bit, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.bit, forks := a, leaves := c } b).leaves ≤ { mode := Mode.bit, forks := a, leaves := c }.forks + { mode := Mode.bit, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.done, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.done, forks := a, leaves := c } b).leaves ≤ { mode := Mode.done, forks := a, leaves := c }.forks + { mode := Mode.done, forks := a, leaves := c }.leaves + 1b:Boola:ℕc:ℕ⊢ (accountStep { mode := Mode.dead, forks := a, leaves := c } b).forks + (accountStep { mode := Mode.dead, forks := a, leaves := c } b).leaves ≤ { mode := Mode.dead, forks := a, leaves := c }.forks + { mode := Mode.dead, forks := a, leaves := c }.leaves + 1 a:ℕc:ℕ⊢ (accountStep { mode := Mode.dead, forks := a, leaves := c } false).forks + (accountStep { mode := Mode.dead, forks := a, leaves := c } false).leaves ≤ { mode := Mode.dead, forks := a, leaves := c }.forks + { mode := Mode.dead, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks + (accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves ≤ { mode := Mode.dead, forks := a, leaves := c }.forks + { mode := Mode.dead, forks := a, leaves := c }.leaves + 1 a:ℕc:ℕ⊢ (accountStep { mode := Mode.tree, forks := a, leaves := c } false).forks + (accountStep { mode := Mode.tree, forks := a, leaves := c } false).leaves ≤ { mode := Mode.tree, forks := a, leaves := c }.forks + { mode := Mode.tree, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.tree, forks := a, leaves := c } true).forks + (accountStep { mode := Mode.tree, forks := a, leaves := c } true).leaves ≤ { mode := Mode.tree, forks := a, leaves := c }.forks + { mode := Mode.tree, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.string, forks := a, leaves := c } false).forks + (accountStep { mode := Mode.string, forks := a, leaves := c } false).leaves ≤ { mode := Mode.string, forks := a, leaves := c }.forks + { mode := Mode.string, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.string, forks := a, leaves := c } true).forks + (accountStep { mode := Mode.string, forks := a, leaves := c } true).leaves ≤ { mode := Mode.string, forks := a, leaves := c }.forks + { mode := Mode.string, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.bit, forks := a, leaves := c } false).forks + (accountStep { mode := Mode.bit, forks := a, leaves := c } false).leaves ≤ { mode := Mode.bit, forks := a, leaves := c }.forks + { mode := Mode.bit, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.bit, forks := a, leaves := c } true).forks + (accountStep { mode := Mode.bit, forks := a, leaves := c } true).leaves ≤ { mode := Mode.bit, forks := a, leaves := c }.forks + { mode := Mode.bit, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.done, forks := a, leaves := c } false).forks + (accountStep { mode := Mode.done, forks := a, leaves := c } false).leaves ≤ { mode := Mode.done, forks := a, leaves := c }.forks + { mode := Mode.done, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.done, forks := a, leaves := c } true).forks + (accountStep { mode := Mode.done, forks := a, leaves := c } true).leaves ≤ { mode := Mode.done, forks := a, leaves := c }.forks + { mode := Mode.done, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.dead, forks := a, leaves := c } false).forks + (accountStep { mode := Mode.dead, forks := a, leaves := c } false).leaves ≤ { mode := Mode.dead, forks := a, leaves := c }.forks + { mode := Mode.dead, forks := a, leaves := c }.leaves + 1a:ℕc:ℕ⊢ (accountStep { mode := Mode.dead, forks := a, leaves := c } true).forks + (accountStep { mode := Mode.dead, forks := a, leaves := c } true).leaves ≤ { mode := Mode.dead, forks := a, leaves := c }.forks + { mode := Mode.dead, forks := a, leaves := c }.leaves + 1 All goals completed! 🐙 a:ℕc:ℕ⊢ a + 1 + c ≤ a + c + 1a:ℕc:ℕ⊢ a + (c + 1) ≤ a + c + 1 All goals completed! 🐙

A prefix bounds the sum of its counters.

theorem account_foldl_sum_le (w : List Bool) : ∀ s, (w.foldl accountStep s).forks + (w.foldl accountStep s).leaves ≤ s.forks + s.leaves + w.length := List.rec (fun _ ↦ w:List Boolx✝:Account⊢ (List.foldl accountStep x✝ []).forks + (List.foldl accountStep x✝ []).leaves ≤ x✝.forks + x✝.leaves + [].length w:List Boolx✝:Account⊢ x✝.forks + x✝.leaves ≤ x✝.forks + x✝.leaves All goals completed! 🐙) (fun b w ih s ↦ w✝:List Boolb:Boolw:List Boolih:∀ (s : Account), (List.foldl accountStep s w).forks + (List.foldl accountStep s w).leaves ≤ s.forks + s.leaves + w.lengths:Account⊢ (List.foldl accountStep s (b :: w)).forks + (List.foldl accountStep s (b :: w)).leaves ≤ s.forks + s.leaves + (b :: w).length w✝:List Boolb:Boolw:List Boolih:∀ (s : Account), (List.foldl accountStep s w).forks + (List.foldl accountStep s w).leaves ≤ s.forks + s.leaves + w.lengths:Accounthi:(List.foldl accountStep (accountStep s b) w).forks + (List.foldl accountStep (accountStep s b) w).leaves ≤ (accountStep s b).forks + (accountStep s b).leaves + w.length⊢ (List.foldl accountStep s (b :: w)).forks + (List.foldl accountStep s (b :: w)).leaves ≤ s.forks + s.leaves + (b :: w).length w✝:List Boolb:Boolw:List Boolih:∀ (s : Account), (List.foldl accountStep s w).forks + (List.foldl accountStep s w).leaves ≤ s.forks + s.leaves + w.lengths:Accounthi:(List.foldl accountStep (accountStep s b) w).forks + (List.foldl accountStep (accountStep s b) w).leaves ≤ (accountStep s b).forks + (accountStep s b).leaves + w.lengthhs:(accountStep s b).forks + (accountStep s b).leaves ≤ s.forks + s.leaves + 1⊢ (List.foldl accountStep s (b :: w)).forks + (List.foldl accountStep s (b :: w)).leaves ≤ s.forks + s.leaves + (b :: w).length w✝:List Boolb:Boolw:List Boolih:∀ (s : Account), (List.foldl accountStep s w).forks + (List.foldl accountStep s w).leaves ≤ s.forks + s.leaves + w.lengths:Accounthi:(List.foldl accountStep (accountStep s b) w).forks + (List.foldl accountStep (accountStep s b) w).leaves ≤ (accountStep s b).forks + (accountStep s b).leaves + w.lengthhs:(accountStep s b).forks + (accountStep s b).leaves ≤ s.forks + s.leaves + 1⊢ (List.foldl accountStep (accountStep s b) w).forks + (List.foldl accountStep (accountStep s b) w).leaves ≤ s.forks + s.leaves + (w.length + 1) All goals completed! 🐙) w

The sum of both counters is bounded by the consumed length plus one.

theorem account_sum_le (w : List Bool) : (account w).forks + (account w).leaves ≤ w.length + 1 := w:List Bool⊢ (account w).forks + (account w).leaves ≤ w.length + 1 w:List Boolh:(List.foldl accountStep initialAccount w).forks + (List.foldl accountStep initialAccount w).leaves ≤ initialAccount.forks + initialAccount.leaves + w.length⊢ (account w).forks + (account w).leaves ≤ w.length + 1 w:List Boolh:(account w).forks + (account w).leaves ≤ 1 + 0 + w.length⊢ (account w).forks + (account w).leaves ≤ w.length + 1 All goals completed! 🐙

Both binary counters fit within the size of the prefix length plus two.

theorem account_size_le (w : List Bool) : (account w).forks.size ≤ (w.length + 2).size ∧ (account w).leaves.size ≤ (w.length + 2).size := w:List Bool⊢ (account w).forks.size ≤ (w.length + 2).size ∧ (account w).leaves.size ≤ (w.length + 2).size w:List Boolh:(account w).forks + (account w).leaves ≤ w.length + 1⊢ (account w).forks.size ≤ (w.length + 2).size ∧ (account w).leaves.size ≤ (w.length + 2).size exact ⟨Counter.size_mono (w:List Boolh:(account w).forks + (account w).leaves ≤ w.length + 1⊢ (account w).forks ≤ w.length + 2 All goals completed! 🐙), Counter.size_mono (w:List Boolh:(account w).forks + (account w).leaves ≤ w.length + 1⊢ (account w).leaves ≤ w.length + 2 All goals completed! 🐙)⟩

The cost of consuming a bit, including an increment and its return scan when needed.

def macroCost (s : Account) (b : Bool) : ℕ := 1 + if s.mode = .tree ∧ b = true then 2 * Counter.flips s.forks.bits + 1 else if s.mode = .string ∧ b = false then 2 * Counter.flips s.leaves.bits + 1 else 0

The accumulated digit changes and update count used in the cost identity.

def accountPotential (s : Account) : ℕ := 2 * (Counter.totalFlips s.forks + Counter.totalFlips s.leaves) + s.forks + s.leaves

The increase in accounting potential is exactly the cost beyond reading the input bit.

theorem macroCost_identity (s : Account) (b : Bool) : macroCost s b + accountPotential s = 1 + accountPotential (accountStep s b) := s:Accountb:Bool⊢ macroCost s b + accountPotential s = 1 + accountPotential (accountStep s b) b:Boolm:Modea:ℕc:ℕ⊢ macroCost { mode := m, forks := a, leaves := c } b + accountPotential { mode := m, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := m, forks := a, leaves := c } b) b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.tree, forks := a, leaves := c } b + accountPotential { mode := Mode.tree, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.tree, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.string, forks := a, leaves := c } b + accountPotential { mode := Mode.string, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.string, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.bit, forks := a, leaves := c } b + accountPotential { mode := Mode.bit, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.bit, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.done, forks := a, leaves := c } b + accountPotential { mode := Mode.done, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.done, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.dead, forks := a, leaves := c } b + accountPotential { mode := Mode.dead, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.dead, forks := a, leaves := c } b) b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.tree, forks := a, leaves := c } b + accountPotential { mode := Mode.tree, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.tree, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.string, forks := a, leaves := c } b + accountPotential { mode := Mode.string, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.string, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.bit, forks := a, leaves := c } b + accountPotential { mode := Mode.bit, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.bit, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.done, forks := a, leaves := c } b + accountPotential { mode := Mode.done, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.done, forks := a, leaves := c } b)b:Boola:ℕc:ℕ⊢ macroCost { mode := Mode.dead, forks := a, leaves := c } b + accountPotential { mode := Mode.dead, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.dead, forks := a, leaves := c } b) a:ℕc:ℕ⊢ macroCost { mode := Mode.dead, forks := a, leaves := c } false + accountPotential { mode := Mode.dead, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.dead, forks := a, leaves := c } false)a:ℕc:ℕ⊢ macroCost { mode := Mode.dead, forks := a, leaves := c } true + accountPotential { mode := Mode.dead, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.dead, forks := a, leaves := c } true) a:ℕc:ℕ⊢ macroCost { mode := Mode.tree, forks := a, leaves := c } false + accountPotential { mode := Mode.tree, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.tree, forks := a, leaves := c } false)a:ℕc:ℕ⊢ macroCost { mode := Mode.tree, forks := a, leaves := c } true + accountPotential { mode := Mode.tree, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.tree, forks := a, leaves := c } true)a:ℕc:ℕ⊢ macroCost { mode := Mode.string, forks := a, leaves := c } false + accountPotential { mode := Mode.string, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.string, forks := a, leaves := c } false)a:ℕc:ℕ⊢ macroCost { mode := Mode.string, forks := a, leaves := c } true + accountPotential { mode := Mode.string, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.string, forks := a, leaves := c } true)a:ℕc:ℕ⊢ macroCost { mode := Mode.bit, forks := a, leaves := c } false + accountPotential { mode := Mode.bit, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.bit, forks := a, leaves := c } false)a:ℕc:ℕ⊢ macroCost { mode := Mode.bit, forks := a, leaves := c } true + accountPotential { mode := Mode.bit, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.bit, forks := a, leaves := c } true)a:ℕc:ℕ⊢ macroCost { mode := Mode.done, forks := a, leaves := c } false + accountPotential { mode := Mode.done, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.done, forks := a, leaves := c } false)a:ℕc:ℕ⊢ macroCost { mode := Mode.done, forks := a, leaves := c } true + accountPotential { mode := Mode.done, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.done, forks := a, leaves := c } true)a:ℕc:ℕ⊢ macroCost { mode := Mode.dead, forks := a, leaves := c } false + accountPotential { mode := Mode.dead, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.dead, forks := a, leaves := c } false)a:ℕc:ℕ⊢ macroCost { mode := Mode.dead, forks := a, leaves := c } true + accountPotential { mode := Mode.dead, forks := a, leaves := c } = 1 + accountPotential (accountStep { mode := Mode.dead, forks := a, leaves := c } true) All goals completed! 🐙 all_goals (a:ℕc:ℕ⊢ 1 + (2 * Counter.flips c.bits + 1) + (2 * (Nat.rec 0 (fun n cost ↦ cost + Counter.flips n.bits) a + Nat.rec 0 (fun n cost ↦ cost + Counter.flips n.bits) c) + a + c) = 1 + (2 * (Nat.rec 0 (fun n cost ↦ cost + Counter.flips n.bits) a + (Nat.rec 0 (fun n cost ↦ cost + Counter.flips n.bits) c + Counter.flips c.bits)) + a + (c + 1)); All goals completed! 🐙)

One combined update of the account and accumulated cost.

def costStep (s : Account × ℕ) (b : Bool) : Account × ℕ := (accountStep s.1 b, s.2 + macroCost s.1 b)

The account component of the cost fold is the ordinary accounting fold.

theorem cost_foldl_fst (w : List Bool) : ∀ s c, (w.foldl costStep (s, c)).1 = w.foldl accountStep s := List.rec (fun _ _ ↦ rfl) (fun b _ ih s c ↦ ih (accountStep s b) (c + macroCost s b)) w

The exact accumulated potential identity for a fold from any initial account and cost.

theorem cost_foldl_identity (w : List Bool) : ∀ s c, (w.foldl costStep (s, c)).2 + accountPotential s = c + w.length + accountPotential (w.foldl accountStep s) := List.rec (fun _ _ ↦ w:List Boolx✝¹:Accountx✝:ℕ⊢ (List.foldl costStep (x✝¹, x✝) []).snd + accountPotential x✝¹ = x✝ + [].length + accountPotential (List.foldl accountStep x✝¹ []) All goals completed! 🐙) (fun b w ih s c ↦ w✝:List Boolb:Boolw:List Boolih:∀ (s : Account) (c : ℕ), (List.foldl costStep (s, c) w).snd + accountPotential s = c + w.length + accountPotential (List.foldl accountStep s w)s:Accountc:ℕ⊢ (List.foldl costStep (s, c) (b :: w)).snd + accountPotential s = c + (b :: w).length + accountPotential (List.foldl accountStep s (b :: w)) w✝:List Boolb:Boolw:List Boolih:∀ (s : Account) (c : ℕ), (List.foldl costStep (s, c) w).snd + accountPotential s = c + w.length + accountPotential (List.foldl accountStep s w)s:Accountc:ℕhi:(List.foldl costStep (accountStep s b, c + macroCost s b) w).snd + accountPotential (accountStep s b) = c + macroCost s b + w.length + accountPotential (List.foldl accountStep (accountStep s b) w)⊢ (List.foldl costStep (s, c) (b :: w)).snd + accountPotential s = c + (b :: w).length + accountPotential (List.foldl accountStep s (b :: w)) w✝:List Boolb:Boolw:List Boolih:∀ (s : Account) (c : ℕ), (List.foldl costStep (s, c) w).snd + accountPotential s = c + w.length + accountPotential (List.foldl accountStep s w)s:Accountc:ℕhi:(List.foldl costStep (accountStep s b, c + macroCost s b) w).snd + accountPotential (accountStep s b) = c + macroCost s b + w.length + accountPotential (List.foldl accountStep (accountStep s b) w)hs:macroCost s b + accountPotential s = 1 + accountPotential (accountStep s b)⊢ (List.foldl costStep (s, c) (b :: w)).snd + accountPotential s = c + (b :: w).length + accountPotential (List.foldl accountStep s (b :: w)) w✝:List Boolb:Boolw:List Boolih:∀ (s : Account) (c : ℕ), (List.foldl costStep (s, c) w).snd + accountPotential s = c + w.length + accountPotential (List.foldl accountStep s w)s:Accountc:ℕhi:(List.foldl costStep (accountStep s b, c + macroCost s b) w).snd + accountPotential (accountStep s b) = c + macroCost s b + w.length + accountPotential (List.foldl accountStep (accountStep s b) w)hs:macroCost s b + accountPotential s = 1 + accountPotential (accountStep s b)⊢ (List.foldl costStep (accountStep s b, c + macroCost s b) w).snd + accountPotential s = c + (w.length + 1) + accountPotential (List.foldl accountStep (accountStep s b) w) w✝:List Boolb:Boolw:List Boolih:∀ (s : Account) (c : ℕ), (List.foldl costStep (s, c) w).snd + accountPotential s = c + w.length + accountPotential (List.foldl accountStep s w)s:Accountc:ℕhi:(List.foldl costStep (accountStep s b, c + macroCost s b) w).snd + accountPotential (accountStep s b) = c + macroCost s b + w.length + accountPotential (List.foldl accountStep (accountStep s b) w)hs:macroCost s b + accountPotential s = 1 + accountPotential (accountStep s b)⊢ (List.foldl costStep (accountStep s b, c + macroCost s b) w).snd + accountPotential s = c + (w.length + 1) + accountPotential (List.foldl accountStep (accountStep s b) w) All goals completed! 🐙) w

Sum of the binary-counter macro costs over the input.

def runCost (w : List Bool) : ℕ := (w.foldl costStep (initialAccount, 0)).2

Extending a prefix adds the macro cost at that prefix's account.

theorem runCost_append (w : List Bool) (b : Bool) : runCost (w ++ [b]) = runCost w + macroCost (account w) b := w:List Boolb:Bool⊢ runCost (w ++ [b]) = runCost w + macroCost (account w) b All goals completed! 🐙

The exact total cost in terms of both monotone counter histories.

theorem runCost_identity (w : List Bool) : runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leaves := w:List Bool⊢ runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leaves w:List Boolh:(List.foldl costStep (initialAccount, 0) w).snd + accountPotential initialAccount = 0 + w.length + accountPotential (List.foldl accountStep initialAccount w)⊢ runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leaves w:List Boolh:runCost w + 3 = 0 + w.length + accountPotential (account w)⊢ runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leaves All goals completed! 🐙

The two-counter implementation has linear total macro cost.

theorem runCost_le (w : List Bool) : runCost w ≤ 6 * w.length + 2 := w:List Bool⊢ runCost w ≤ 6 * w.length + 2 w:List Boolhi:runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leaves⊢ runCost w ≤ 6 * w.length + 2 w:List Boolhi:runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leavesha:Counter.totalFlips (account w).forks ≤ 2 * (account w).forks⊢ runCost w ≤ 6 * w.length + 2 w:List Boolhi:runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leavesha:Counter.totalFlips (account w).forks ≤ 2 * (account w).forkshb:Counter.totalFlips (account w).leaves ≤ 2 * (account w).leaves⊢ runCost w ≤ 6 * w.length + 2 w:List Boolhi:runCost w + 3 = w.length + 2 * (Counter.totalFlips (account w).forks + Counter.totalFlips (account w).leaves) + (account w).forks + (account w).leavesha:Counter.totalFlips (account w).forks ≤ 2 * (account w).forkshb:Counter.totalFlips (account w).leaves ≤ 2 * (account w).leaveshs:(account w).forks + (account w).leaves ≤ w.length + 1⊢ runCost w ≤ 6 * w.length + 2 All goals completed! 🐙

The accounting state at the next prefix is one update from the current prefix.

theorem account_take_succ (w : List Bool) (t : ℕ) (h : t < w.length) : account (w.take (t + 1)) = accountStep (account (w.take t)) w[t] := w:List Boolt:ℕh:t < w.length⊢ account (List.take (t + 1) w) = accountStep (account (List.take t w)) w[t] All goals completed! 🐙

Extending a prefix adds one input-and-counter macro cost.

theorem runCost_take_succ (w : List Bool) (t : ℕ) (h : t < w.length) : runCost (w.take (t + 1)) = runCost (w.take t) + macroCost (account (w.take t)) w[t] := w:List Boolt:ℕh:t < w.length⊢ runCost (List.take (t + 1) w) = runCost (List.take t w) + macroCost (account (List.take t w)) w[t] All goals completed! 🐙

Both counters of every prefix fit in the binary width of the whole input length plus two.

theorem prefix_size_le (w : List Bool) (t : ℕ) : (account (w.take t)).forks.size ≤ (w.length + 2).size ∧ (account (w.take t)).leaves.size ≤ (w.length + 2).size := w:List Boolt:ℕ⊢ (account (List.take t w)).forks.size ≤ (w.length + 2).size ∧ (account (List.take t w)).leaves.size ≤ (w.length + 2).size w:List Boolt:ℕh:(account (List.take t w)).forks.size ≤ ((List.take t w).length + 2).size ∧ (account (List.take t w)).leaves.size ≤ ((List.take t w).length + 2).size⊢ (account (List.take t w)).forks.size ≤ (w.length + 2).size ∧ (account (List.take t w)).leaves.size ≤ (w.length + 2).size w:List Boolt:ℕh:(account (List.take t w)).forks.size ≤ ((List.take t w).length + 2).size ∧ (account (List.take t w)).leaves.size ≤ ((List.take t w).length + 2).sizehw:((List.take t w).length + 2).size ≤ (w.length + 2).size⊢ (account (List.take t w)).forks.size ≤ (w.length + 2).size ∧ (account (List.take t w)).leaves.size ≤ (w.length + 2).size All goals completed! 🐙

The chosen width always accommodates the initialization markers.

theorem width_pos (n : ℕ) : 0 < (n + 2).size := n:ℕ⊢ 0 < (n + 2).size n:ℕh:n + 2 < 2 ^ (n + 2).size⊢ 0 < (n + 2).size n:ℕh:n + 2 < 2 ^ (n + 2).sizehz:(n + 2).size = 0⊢ 0 < (n + 2).sizen:ℕh:n + 2 < 2 ^ (n + 2).sizehz:¬(n + 2).size = 0⊢ 0 < (n + 2).size n:ℕh:n + 2 < 2 ^ (n + 2).sizehz:(n + 2).size = 0⊢ 0 < (n + 2).size n:ℕh:n + 2 < 2 ^ 0hz:(n + 2).size = 0⊢ 0 < (n + 2).size n:ℕh:n + 2 < 1hz:(n + 2).size = 0⊢ 0 < (n + 2).size All goals completed! 🐙 n:ℕh:n + 2 < 2 ^ (n + 2).sizehz:¬(n + 2).size = 0⊢ 0 < (n + 2).size All goals completed! 🐙
end Geb.BitTree.BinaryMachine