Geb
Prototypes
Computability
BitTree
Elias
RepresentationLowerBound

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.List.Nodup
public import Batteries.Data.List.Perm
public import Geb.Prototypes.Computability.BitTree.Encoding

set_option doc.verso true

Counting lower bound for lossless tree representations

For fixed fork count I and total payload length B, every injective binary representation has worst-case length at least B. A fixed comb shape already contains all 2^B choices for its last leaf's payload. There are only 2^B - 1 binary words shorter than B, even when codewords need not be prefix-free.

Main definitions

words enumerates fixed-length bitstrings using list sections.
payloadComb embeds arbitrary bitstrings into trees with a prescribed fork count.

Main statements

bitstring_representation_lower_bound proves the finite counting bound.
tree_representation_lower_bound transfers it to trees of fixed size.

Tags

binary tree, representation size, counting, information lower bound

@[expose] public sectionnamespace Geb.BitTree.Elias

All binary words of the given length.

def words (n : ℕ) : List (List Bool) := (List.replicate n [false, true]).sections

Enumeration extends every shorter word by each possible next bit.

theorem words_succ (n : ℕ) :
    words (n + 1) = (words n).flatMap fun w ↦ [false :: w, true :: w] := byn:ℕ⊢ words (n + 1) = List.flatMap (fun w ↦ [false :: w, true :: w]) (words n)
  simp only [words, List.replicate_succ, List.sections, List.map_cons, List.map_nil]All goals completed! 🐙

Fixed-length enumeration contains exactly the words of that length.

theorem mem_words (n : ℕ) : ∀ w, w ∈ words n ↔ w.length = n := byn:ℕ⊢ ∀ (w : List Bool), w ∈ words n ↔ w.length = n
  refine Nat.rec ?_ ?_ nrefine_1n:ℕ⊢ ∀ (w : List Bool), w ∈ words Nat.zero ↔ w.length = Nat.zerorefine_2n:ℕ⊢ ∀ (n : ℕ), (∀ (w : List Bool), w ∈ words n ↔ w.length = n) → ∀ (w : List Bool), w ∈ words n.succ ↔ w.length = n.succ
  ·refine_1n:ℕ⊢ ∀ (w : List Bool), w ∈ words Nat.zero ↔ w.length = Nat.zero intro wrefine_1n:ℕw:List Bool⊢ w ∈ words Nat.zero ↔ w.length = Nat.zero
    simp [words]All goals completed! 🐙
  ·refine_2n:ℕ⊢ ∀ (n : ℕ), (∀ (w : List Bool), w ∈ words n ↔ w.length = n) → ∀ (w : List Bool), w ∈ words n.succ ↔ w.length = n.succ intro n ih wrefine_2n✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ w ∈ words n.succ ↔ w.length = n.succ
    rw [words_succ,refine_2n✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ w ∈ List.flatMap (fun w ↦ [false :: w, true :: w]) (words n) ↔ w.length = n.succ List.mem_flatMaprefine_2n✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ (∃ a ∈ words n, w ∈ [false :: a, true :: a]) ↔ w.length = n.succ]refine_2n✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ (∃ a ∈ words n, w ∈ [false :: a, true :: a]) ↔ w.length = n.succ
    constructorrefine_2.mpn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ (∃ a ∈ words n, w ∈ [false :: a, true :: a]) → w.length = n.succrefine_2.mprn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ w.length = n.succ → ∃ a ∈ words n, w ∈ [false :: a, true :: a]
    ·refine_2.mpn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ (∃ a ∈ words n, w ∈ [false :: a, true :: a]) → w.length = n.succ rintro ⟨v, hv, hw⟩refine_2.mpn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolv:List Boolhv:v ∈ words nhw:w ∈ [false :: v, true :: v]⊢ w.length = n.succ
      have hl := (ih v).mp hvrefine_2.mpn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolv:List Boolhv:v ∈ words nhw:w ∈ [false :: v, true :: v]hl:v.length = n⊢ w.length = n.succ
      simp only [List.mem_cons, List.not_mem_nil, or_false] at hwrefine_2.mpn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolv:List Boolhv:v ∈ words nhl:v.length = nhw:w = false :: v ∨ w = true :: v⊢ w.length = n.succ
      rcases hw with rfl | rflrefine_2.mp.inln✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nv:List Boolhv:v ∈ words nhl:v.length = n⊢ (false :: v).length = n.succrefine_2.mp.inrn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nv:List Boolhv:v ∈ words nhl:v.length = n⊢ (true :: v).length = n.succ <;>refine_2.mp.inln✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nv:List Boolhv:v ∈ words nhl:v.length = n⊢ (false :: v).length = n.succrefine_2.mp.inrn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nv:List Boolhv:v ∈ words nhl:v.length = n⊢ (true :: v).length = n.succ simp only [List.length_cons, hl]All goals completed! 🐙
    ·refine_2.mprn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Bool⊢ w.length = n.succ → ∃ a ∈ words n, w ∈ [false :: a, true :: a] intro hwrefine_2.mprn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolhw:w.length = n.succ⊢ ∃ a ∈ words n, w ∈ [false :: a, true :: a]
      cases w with
      | nil =>refine_2.mpr.niln✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nhw:[].length = n.succ⊢ ∃ a ∈ words n, [] ∈ [false :: a, true :: a] simp only [List.length_nil] at hwrefine_2.mpr.niln✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nhw:0 = n.succ⊢ ∃ a ∈ words n, [] ∈ [false :: a, true :: a]; omegaAll goals completed! 🐙
      | cons b w =>refine_2.mpr.consn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nb:Boolw:List Boolhw:(b :: w).length = n.succ⊢ ∃ a ∈ words n, b :: w ∈ [false :: a, true :: a]
        refine ⟨w, (ih w).mpr (byn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nb:Boolw:List Boolhw:(b :: w).length = n.succ⊢ w.length = n simp only [List.length_cons] at hwn✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nb:Boolw:List Boolhw:w.length + 1 = n.succ⊢ w.length = n; omegaAll goals completed! 🐙), ?_⟩
        cases brefine_2.mpr.cons.falsen✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolhw:(false :: w).length = n.succ⊢ false :: w ∈ [false :: w, true :: w]refine_2.mpr.cons.truen✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolhw:(true :: w).length = n.succ⊢ true :: w ∈ [false :: w, true :: w] <;>refine_2.mpr.cons.falsen✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolhw:(false :: w).length = n.succ⊢ false :: w ∈ [false :: w, true :: w]refine_2.mpr.cons.truen✝:ℕn:ℕih:∀ (w : List Bool), w ∈ words n ↔ w.length = nw:List Boolhw:(true :: w).length = n.succ⊢ true :: w ∈ [false :: w, true :: w] simpAll goals completed! 🐙

There are exactly two to the power of the length binary words.

theorem length_words : ∀ n, (words n).length = 2 ^ n := by⊢ ∀ (n : ℕ), (words n).length = 2 ^ n
  refine Nat.rec rfl ?_⊢ ∀ (n : ℕ), (words n).length = 2 ^ n → (words n.succ).length = 2 ^ n.succ
  intro n ihn:ℕih:(words n).length = 2 ^ n⊢ (words n.succ).length = 2 ^ n.succ
  rw [words_succ,n:ℕih:(words n).length = 2 ^ n⊢ (List.flatMap (fun w ↦ [false :: w, true :: w]) (words n)).length = 2 ^ n.succ List.length_flatMapn:ℕih:(words n).length = 2 ^ n⊢ (List.map (fun a ↦ [false :: a, true :: a].length) (words n)).sum = 2 ^ n.succ]n:ℕih:(words n).length = 2 ^ n⊢ (List.map (fun a ↦ [false :: a, true :: a].length) (words n)).sum = 2 ^ n.succ
  simp only [List.length_cons, List.length_nil, List.map_const', List.sum_replicate,
    ih, Nat.pow_succ, Nat.nsmul_eq_mul]All goals completed! 🐙

Fixed-length enumeration has no duplicate words.

theorem nodup_words : ∀ n, (words n).Nodup := by⊢ ∀ (n : ℕ), (words n).Nodup
  refine Nat.rec (by⊢ (words Nat.zero).Nodup simp [words]All goals completed! 🐙) ?_
  intro n ihn:ℕih:(words n).Nodup⊢ (words n.succ).Nodup
  rw [words_succ,n:ℕih:(words n).Nodup⊢ (List.flatMap (fun w ↦ [false :: w, true :: w]) (words n)).Nodup List.nodup_flatMapn:ℕih:(words n).Nodup⊢ (∀ x ∈ words n, [false :: x, true :: x].Nodup) ∧
  List.Pairwise (Function.onFun List.Disjoint fun w ↦ [false :: w, true :: w]) (words n)]n:ℕih:(words n).Nodup⊢ (∀ x ∈ words n, [false :: x, true :: x].Nodup) ∧
  List.Pairwise (Function.onFun List.Disjoint fun w ↦ [false :: w, true :: w]) (words n)
  refine ⟨fun w _ ↦ byn:ℕih:(words n).Nodupw:List Boolx✝:w ∈ words n⊢ [false :: w, true :: w].Nodup simpAll goals completed! 🐙, ih.imp ?_⟩
  intro a b habn:ℕih:(words n).Nodupa:List Boolb:List Boolhab:a ≠ b⊢ Function.onFun List.Disjoint (fun w ↦ [false :: w, true :: w]) a b
  simp [List.disjoint_left, hab]All goals completed! 🐙

All binary words strictly shorter than the given bound.

def shortWords (n : ℕ) : List (List Bool) := (List.range n).flatMap words

Membership in the bounded enumeration is exactly the strict length bound.

theorem mem_shortWords (n : ℕ) (w : List Bool) : w ∈ shortWords n ↔ w.length < n := byn:ℕw:List Bool⊢ w ∈ shortWords n ↔ w.length < n
  simp only [shortWords, List.mem_flatMap, List.mem_range, mem_words]n:ℕw:List Bool⊢ (∃ a < n, w.length = a) ↔ w.length < n
  exact ⟨fun ⟨k, hk, he⟩ ↦ he ▸ hk, fun h ↦ ⟨w.length, h, rfl⟩⟩All goals completed! 🐙

The number of words shorter than a bound is one less than its power of two.

theorem length_shortWords : ∀ n, (shortWords n).length + 1 = 2 ^ n := by⊢ ∀ (n : ℕ), (shortWords n).length + 1 = 2 ^ n
  refine Nat.rec rfl ?_⊢ ∀ (n : ℕ), (shortWords n).length + 1 = 2 ^ n → (shortWords n.succ).length + 1 = 2 ^ n.succ
  intro n ihn:ℕih:(shortWords n).length + 1 = 2 ^ n⊢ (shortWords n.succ).length + 1 = 2 ^ n.succ
  have he : shortWords (n + 1) = shortWords n ++ words n := by⊢ ∀ (n : ℕ), (shortWords n).length + 1 = 2 ^ n
    simp only [shortWords, List.range_succ, List.flatMap_append, List.flatMap_cons,
      List.flatMap_nil, List.append_nil]n:ℕih:(shortWords n).length + 1 = 2 ^ nhe:shortWords (n + 1) = shortWords n ++ words n⊢ (shortWords n.succ).length + 1 = 2 ^ n.succ
  rw [he,n:ℕih:(shortWords n).length + 1 = 2 ^ nhe:shortWords (n + 1) = shortWords n ++ words n⊢ (shortWords n ++ words n).length + 1 = 2 ^ n.succ List.length_append,n:ℕih:(shortWords n).length + 1 = 2 ^ nhe:shortWords (n + 1) = shortWords n ++ words n⊢ (shortWords n).length + (words n).length + 1 = 2 ^ n.succ length_words,n:ℕih:(shortWords n).length + 1 = 2 ^ nhe:shortWords (n + 1) = shortWords n ++ words n⊢ (shortWords n).length + 2 ^ n + 1 = 2 ^ n.succ Nat.pow_succn:ℕih:(shortWords n).length + 1 = 2 ^ nhe:shortWords (n + 1) = shortWords n ++ words n⊢ (shortWords n).length + 2 ^ n + 1 = 2 ^ n * 2]n:ℕih:(shortWords n).length + 1 = 2 ^ nhe:shortWords (n + 1) = shortWords n ++ words n⊢ (shortWords n).length + 2 ^ n + 1 = 2 ^ n * 2
  omegaAll goals completed! 🐙

An injective encoding of all fixed-length words cannot shorten every word.

theorem bitstring_representation_lower_bound (code : List Bool → List Bool)
    (hinj : Function.Injective code) (bits bound : ℕ)
    (hbound : ∀ w, w.length = bits → (code w).length ≤ bound) : bits ≤ bound := bycode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ bound⊢ bits ≤ bound
  have hsub : (words bits).map code ⊆ shortWords (bound + 1) := by
    intro w hwcode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundw:List Boolhw:w ∈ List.map code (words bits)⊢ w ∈ shortWords (bound + 1)
    obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hwcode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundv:List Boolhv:v ∈ words bitshw:code v ∈ List.map code (words bits)⊢ code v ∈ shortWords (bound + 1)
    exact (mem_shortWords _ _).mpr (bycode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundv:List Boolhv:v ∈ words bitshw:code v ∈ List.map code (words bits)⊢ (code v).length < bound + 1 have := hbound v ((mem_words _ _).mp hv)code:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundv:List Boolhv:v ∈ words bitshw:code v ∈ List.map code (words bits)this:(code v).length ≤ bound⊢ (code v).length < bound + 1; omegaAll goals completed! 🐙)code:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)⊢ bits ≤ bound
  have hlen := (List.subperm_of_subset ((nodup_words bits).map hinj) hsub).length_lecode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:(List.map code (words bits)).length ≤ (shortWords (bound + 1)).length⊢ bits ≤ bound
  rw [List.length_map,code:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:(words bits).length ≤ (shortWords (bound + 1)).length⊢ bits ≤ bound length_wordscode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).length⊢ bits ≤ bound] at hlencode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).length⊢ bits ≤ bound
  have hs := length_shortWords (bound + 1)code:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)⊢ bits ≤ bound
  by_cases h : bits ≤ boundposcode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)h:bits ≤ bound⊢ bits ≤ boundnegcode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)h:¬bits ≤ bound⊢ bits ≤ bound
  ·poscode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)h:bits ≤ bound⊢ bits ≤ bound exact hAll goals completed! 🐙
  ·negcode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)h:¬bits ≤ bound⊢ bits ≤ bound have hp : 2 ^ (bound + 1) ≤ 2 ^ bits := Nat.pow_le_pow_right (bycode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)h:¬bits ≤ bound⊢ 2 > 0 decideAll goals completed! 🐙) (bycode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)h:¬bits ≤ bound⊢ bound + 1 ≤ bits omegaAll goals completed! 🐙)negcode:List Bool → List Boolhinj:Function.Injective codebits:ℕbound:ℕhbound:∀ (w : List Bool), w.length = bits → (code w).length ≤ boundhsub:List.map code (words bits) ⊆ shortWords (bound + 1)hlen:2 ^ bits ≤ (shortWords (bound + 1)).lengthhs:(shortWords (bound + 1)).length + 1 = 2 ^ (bound + 1)h:¬bits ≤ boundhp:2 ^ (bound + 1) ≤ 2 ^ bits⊢ bits ≤ bound
    omegaAll goals completed! 🐙

A fixed right comb with empty left leaves and one variable last payload.

def payloadComb (forks : ℕ) (w : List Bool) : Tree :=
  Nat.rec (leaf w) (fun _ t ↦ fork (leaf []) t) forks

The payload stored at the rightmost leaf.

def lastPayload : Tree → List Bool := WType.elim (List Bool) fun x ↦
  match x with
  | ⟨some s, _⟩ => s
  | ⟨none, f⟩ => f true

Reading the last leaf recovers the word used to build a comb.

theorem lastPayload_payloadComb (w : List Bool) : ∀ forks,
    lastPayload (payloadComb forks w) = w :=
  Nat.rec rfl (fun _ ih ↦ ih)

Varying the last payload gives distinct trees.

theorem payloadComb_injective (forks : ℕ) : Function.Injective (payloadComb forks) := byforks:ℕ⊢ Function.Injective (payloadComb forks)
  intro v w hforks:ℕv:List Boolw:List Boolh:payloadComb forks v = payloadComb forks w⊢ v = w
  have he := congrArg lastPayload hforks:ℕv:List Boolw:List Boolh:payloadComb forks v = payloadComb forks whe:lastPayload (payloadComb forks v) = lastPayload (payloadComb forks w)⊢ v = w
  simpa only [lastPayload_payloadComb] using heAll goals completed! 🐙

The comb fixes the fork count while retaining the full payload length.

theorem counts_payloadComb (w : List Bool) : ∀ forks,
    counts (payloadComb forks w) = (forks, forks + 1, w.length) := byw:List Bool⊢ ∀ (forks : ℕ), counts (payloadComb forks w) = (forks, forks + 1, w.length)
  refine Nat.rec rfl ?_w:List Bool⊢ ∀ (n : ℕ),
  counts (payloadComb n w) = (n, n + 1, w.length) → counts (payloadComb n.succ w) = (n.succ, n.succ + 1, w.length)
  intro forks ihw:List Boolforks:ℕih:counts (payloadComb forks w) = (forks, forks + 1, w.length)⊢ counts (payloadComb forks.succ w) = (forks.succ, forks.succ + 1, w.length)
  change counts (fork (leaf []) (payloadComb forks w)) = _w:List Boolforks:ℕih:counts (payloadComb forks w) = (forks, forks + 1, w.length)⊢ counts (fork (leaf []) (payloadComb forks w)) = (forks.succ, forks.succ + 1, w.length)
  rw [counts_fork,w:List Boolforks:ℕih:counts (payloadComb forks w) = (forks, forks + 1, w.length)⊢ ((counts (leaf [])).1 + (counts (payloadComb forks w)).1 + 1,
    (counts (leaf [])).2.1 + (counts (payloadComb forks w)).2.1,
    (counts (leaf [])).2.2 + (counts (payloadComb forks w)).2.2) =
  (forks.succ, forks.succ + 1, w.length) counts_leaf,w:List Boolforks:ℕih:counts (payloadComb forks w) = (forks, forks + 1, w.length)⊢ ((0, 1, [].length).1 + (counts (payloadComb forks w)).1 + 1, (0, 1, [].length).2.1 + (counts (payloadComb forks w)).2.1,
    (0, 1, [].length).2.2 + (counts (payloadComb forks w)).2.2) =
  (forks.succ, forks.succ + 1, w.length) ihw:List Boolforks:ℕih:counts (payloadComb forks w) = (forks, forks + 1, w.length)⊢ ((0, 1, [].length).1 + (forks, forks + 1, w.length).1 + 1, (0, 1, [].length).2.1 + (forks, forks + 1, w.length).2.1,
    (0, 1, [].length).2.2 + (forks, forks + 1, w.length).2.2) =
  (forks.succ, forks.succ + 1, w.length)]w:List Boolforks:ℕih:counts (payloadComb forks w) = (forks, forks + 1, w.length)⊢ ((0, 1, [].length).1 + (forks, forks + 1, w.length).1 + 1, (0, 1, [].length).2.1 + (forks, forks + 1, w.length).2.1,
    (0, 1, [].length).2.2 + (forks, forks + 1, w.length).2.2) =
  (forks.succ, forks.succ + 1, w.length)
  simp only [List.length_nil, Nat.zero_add, Nat.add_comm 1]All goals completed! 🐙

Any lossless binary code for trees needs at least the total payload length in the worst case.

theorem tree_representation_lower_bound (code : Tree → List Bool)
    (hinj : Function.Injective code) (forks bits bound : ℕ)
    (hbound : ∀ t, (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ bound) :
    bits ≤ bound := bycode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ bound⊢ bits ≤ bound
  apply bitstring_representation_lower_bound (fun w ↦ code (payloadComb forks w))
    (hinj.comp (payloadComb_injective forks)) bits boundcode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ bound⊢ ∀ (w : List Bool), w.length = bits → (code (payloadComb forks w)).length ≤ bound
  intro w hwcode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (code (payloadComb forks w)).length ≤ bound
  apply hbound (payloadComb forks w)acode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (counts (payloadComb forks w)).1 = forksacode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (counts (payloadComb forks w)).2.2 = bits
  ·acode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (counts (payloadComb forks w)).1 = forks rw [counts_payloadCombacode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (forks, forks + 1, w.length).1 = forks]All goals completed! 🐙
  ·acode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (counts (payloadComb forks w)).2.2 = bits rw [counts_payloadComb,acode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (forks, forks + 1, w.length).2.2 = bits hwacode:Tree → List Boolhinj:Function.Injective codeforks:ℕbits:ℕbound:ℕhbound:∀ (t : Tree), (counts t).1 = forks → (counts t).2.2 = bits → (code t).length ≤ boundw:List Boolhw:w.length = bits⊢ (forks, forks + 1, bits).2.2 = bits]All goals completed! 🐙

end Geb.BitTree.Elias