ForestCode.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

A finite code for rooted ordered forests

First-child / next-sibling representation turns a rooted ordered forest into a binary tree. One bit records a leaf; a nonleaf uses a marker and a vertex-type bit. The resulting code has exactly 3*n+1 bits.

def OAI.TwoPointCorrelations.forestBits line 21
Source documentation
Prefix encoding of a typed plane forest in binary-tree representation.
```
def forestBits : BinaryTree Bool → List Bool
  | .nil => [false]
  | .node b l r => true :: b :: (forestBits l ++ forestBits r)
```
theorem OAI.TwoPointCorrelations.forestBits_length line 25

def OAI.TwoPointCorrelations.parseForestBits line 33

Source documentation

Fuel is the maximal number of nested nodes plus one.

def parseForestBits : ℕ → List Bool → Option (BinaryTree Bool × List Bool)
  | 0, _ => none
  | _ + 1, false :: rest => some (.nil, rest)
  | fuel + 1, true :: b :: rest => do
      let (l, rest') ← parseForestBits fuel rest
      let (r, rest'') ← parseForestBits fuel rest'
      some (.node b l r, rest'')
  | _ + 1, _ => none

theorem OAI.TwoPointCorrelations.parseForestBits_encode line 42
def OAI.TwoPointCorrelations.paddedForestBits line 60
Source documentation
Padding to a common length preserves injectivity, since parsing stops at the exact end of the represented tree.
```
def paddedForestBits (N : ℕ) (t : BinaryTree Bool) : List Bool :=
…
```
lemma OAI.TwoPointCorrelations.paddedForestBits_length line 63
theorem OAI.TwoPointCorrelations.paddedForestBits_injective line 68
def OAI.TwoPointCorrelations.boundedForestCode line 80
Source documentation
Fixed-length bit vectors enumerate every forest with at most N vertices.
```
def boundedForestCode (N : ℕ) (t : {t : BinaryTree Bool // t.numNodes ≤ N}) :
    Fin (3 * N + 1) → Bool :=
…
```
theorem OAI.TwoPointCorrelations.boundedForestCode_injective line 85
theorem OAI.TwoPointCorrelations.card_bounded_forests line 96
Source documentation
Exponential, coefficient-independent count for typed plane-forest shapes.
```
theorem card_bounded_forests (N : ℕ) :
    Nat.card {t : BinaryTree Bool // t.numNodes ≤ N} ≤ 2 ^ (3 * N + 1) := by
…
```