Dyck words and proper binary trees

Formalizes the grammar, tree encoding, graded correspondence, and Catalan cardinality in Lem:optimal_dyck (main.tex:337–342).

The Dyck language (main.tex:337)

inductive Nock.Dyck : List Bool → Prop

Prelude of Lem:optimal_dyck (main.tex:337). L_dk = { w ∈ {0,1}^* | w=ε or ∃ w₁,w₂ ∈ L_dk s.t. w = 0 w₁ 1 w₂ }.

• eps : Dyck []
• cat {w₁ w₂ : List Bool} : Dyck w₁ → Dyck w₂ → Dyck (false :: w₁ ++ true :: w₂)

Proper binary tree shapes = L_full_BT (main.tex:318–327)

inductive Nock.BTree : Type

Def:Proper_BT (main.tex:318–327). L_full_BT = { t ∈ T | (size(t)=1) ∪ (left(t) ∈ L_full_BT ∩ right(t) ∈ L_full_BT ∩ (left(t) ∩ right(t)=∅)) }; L^λ_full_BT = { t ∈ L_full_BT | size(t)=λ }.

• leaf : BTree
• node : BTree → BTree → BTree

@[instance_reducible]

instance Nock.instReprBTree : Repr BTree

Equations

• Nock.instReprBTree = { reprPrec := Nock.instReprBTree.repr }

def Nock.instReprBTree.repr : BTree → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Nock.instReprBTree.repr Nock.BTree.leaf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.BTree.leaf")).group prec✝

def Nock.instDecidableEqBTree.decEq (x✝ x✝¹ : BTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Nock.instDecidableEqBTree.decEq Nock.BTree.leaf Nock.BTree.leaf = isTrue ⋯
• Nock.instDecidableEqBTree.decEq Nock.BTree.leaf (a.node a_1) = isFalse ⋯
• Nock.instDecidableEqBTree.decEq (a.node a_1) Nock.BTree.leaf = isFalse ⋯

@[instance_reducible]

instance Nock.instDecidableEqBTree : DecidableEq BTree

Equations

• Nock.instDecidableEqBTree = Nock.instDecidableEqBTree.decEq

@[instance_reducible]

instance Nock.instInhabitedBTree : Inhabited BTree

Equations

• Nock.instInhabitedBTree = { default := Nock.instInhabitedBTree.default }

def Nock.BTree.size : BTree → ℕ

Total node count of a shape (matches Noun.size).

Equations

• Nock.BTree.leaf.size = 1
• (l.node r).size = 1 + l.size + r.size

def Nock.BTree.encode : BTree → List Bool

The Dyck encoding of a proper binary tree (main.tex:337): leaf ↦ ε, node l r ↦ 0 · encode l · 1 · encode r.

Equations

• Nock.BTree.leaf.encode = []
• (l.node r).encode = false :: l.encode ++ true :: r.encode

theorem Nock.BTree.encode_length_add_one (t : BTree) : t.encode.length + 1 = t.size

A Dyck word encoding a tree has length size − 1 (each internal node contributes the pair 0…1). Stated additively to avoid truncated subtraction.

encode lands in the Dyck language, and is onto it (main.tex:340)

theorem Nock.BTree.dyck_encode (t : BTree) : Dyck t.encode

Every tree encodes to a Dyck word.

theorem Nock.BTree.exists_encode_of_dyck {w : List Bool} (h : Dyck w) : ∃ (t : BTree), t.encode = w

Every Dyck word is the encoding of some tree (surjectivity of encode onto L_dk).

A greedy parser, to pin down injectivity of encode

`decode fuel w` parses exactly one tree off the front of `w`, returning the tree and the
unconsumed suffix.  A leading `0` (`false`) starts a `node`; anything else (a leading `1`
or the empty word) is a `leaf` consuming nothing.  This is the algorithmic inverse of
`encode`; `decode_encode` proves the round-trip, which yields injectivity. 

def Nock.BTree.decode : ℕ → List Bool → Option (BTree × List Bool)

Parse one binary tree from a Dyck prefix, returning the tree and unconsumed suffix.

Equations

• One or more equations did not get rendered due to their size.
• Nock.BTree.decode 0 x✝ = none
• Nock.BTree.decode n.succ x✝ = some (Nock.BTree.leaf, x✝)

Round-trip: decode inverts encode, hence encode is injective

theorem Nock.BTree.decode_encode (t : BTree) (fuel : ℕ) (rest : List Bool) : t.size ≤ fuel → rest = [] ∨ rest.head? = some true → decode fuel (t.encode ++ rest) = some (t, rest)

The greedy parser recovers the encoded tree and returns the untouched suffix, provided the fuel covers the tree's size and the suffix is not "open"-led (which is exactly the invariant maintained by the recursion: a left subtree is followed by its closing 1, a right subtree by the parent's suffix).

theorem Nock.BTree.encode_injective {t₁ t₂ : BTree} (h : t₁.encode = t₂.encode) : t₁ = t₂

encode is injective: distinct shapes have distinct Dyck words.

Lem:optimal_dyck (main.tex:340–342)

theorem Nock.BTree.dyck_iff_encode {w : List Bool} : Dyck w ↔ ∃ (t : BTree), t.encode = w

Lem:optimal_dyck (main.tex:340–342). L_dk ≡ L_full_BT.

theorem Nock.BTree.dyck_length_graded {w : List Bool} (t : BTree) (ht : t.encode = w) (lam : ℕ) : w.length = 2 * lam ↔ t.size = 2 * lam + 1

Lem:optimal_dyck (main.tex:340–342). ∀λ, L^{2λ}_dk ≡ L^{2λ+1}_full_BT.

Connection to Noun: a noun is a shape (BTree) plus leaf data (main.tex:347)

def Nock.Noun.shape : Noun → BTree

The shape of a noun: erase the leaf data, leaving a proper binary tree (L_full_BT). The paper's noun (t, dt) pairs this shape (encoded as the Dyck word t) with the leaf array dt; the Dyck bijection above governs the t component.

Equations

• (Nock.Noun.atom a).shape = Nock.BTree.leaf
• (l.cell r).shape = l.shape.node r.shape

theorem Nock.Noun.shape_size (n : Noun) : n.shape.size = n.size

The shape preserves leaf and node counts (Noun.size = BTree.size ∘ shape).

def Nock.Noun.dyckWord (n : Noun) : List Bool

The Dyck word of a noun: the encoding of its shape. By Lem:pbt_size (main.tex:333) a noun with λ leaves has size 2λ − 1, so its Dyck word has length 2λ − 2 = 2(λ−1), matching the paper's L^{2(λ−1)}_dk component of a noun (main.tex:1164).

Equations

• n.dyckWord = n.shape.encode

theorem Nock.Noun.dyckWord_length (n : Noun) : n.dyckWord.length + 2 = 2 * n.leaves

A noun's Dyck word has length 2·leaves − 2 = 2(λ−1) (main.tex:1164).

Leaf array + Def "noun" uniqueness (main.tex:347)

A noun is `(t, dt)` = Dyck shape + DFS leaf array.  These live here (not in NPR) so the
Pure Nock language closure can talk about uniqueness without importing Field/Goldilocks. 

def Nock.Noun.leafList : Noun → List ℕ

The leaf values of a noun in left-to-right (DFS) order — the paper's leaf array dt (main.tex:1164), here over Nat (cast into the field at the NPR layer).

Equations

• (Nock.Noun.atom a).leafList = [a]
• (l.cell r).leafList = l.leafList ++ r.leafList

@[simp]

theorem Nock.Noun.leafList_length (n : Noun) : n.leafList.length = n.leaves

theorem Nock.Noun.shape_leaves_eq {n₁ n₂ : Noun} (h : n₁.shape = n₂.shape) : n₁.leaves = n₂.leaves

Equal shape ⇒ equal leaf count: the Dyck shape already determines λ (Lem:pbt_size, main.tex:333), so it constrains how the leaf array splits between the two subtrees.

theorem Nock.Noun.eq_of_shape_leafList {n₁ n₂ : Noun} : n₁.shape = n₂.shape → n₁.leafList = n₂.leafList → n₁ = n₂

Reconstruction. If two nouns have the same shape (Dyck word) and the same leaf array, they are the same noun: the shape fixes the tree structure and the leaf list fills the leaves in DFS order, leaving no ambiguity.

theorem Nock.Noun.noun_dyck_leaf_injective : Function.Injective fun (n : Noun) => (n.dyckWord, n.leafList)

Def "noun" uniqueness (main.tex:347). The map sending a noun to its Dyck word + leaf array, n ↦ (n.dyckWord, n.leafList), is injective. This is the paper's claim that the tuple (t, dt) "corresponds to a unique noun" (main.tex:345,347).

Catalan cardinality |L^{2λ}_dk| = C_λ (Lem:optimal_dyck, main.tex:341)

def Nock.BTree.toBin : BTree → BinaryTree Unit

The shape isomorphism to Mathlib's BinaryTree: a proper-binary-tree leaf is Mathlib's empty leaf nil; a node is a Mathlib node carrying the unit value.

Equations

• Nock.BTree.leaf.toBin = BinaryTree.nil
• (l.node r).toBin = BinaryTree.node () l.toBin r.toBin

def Nock.BTree.ofBin : BinaryTree Unit → BTree

Inverse of toBin.

Equations

• Nock.BTree.ofBin BinaryTree.nil = Nock.BTree.leaf
• Nock.BTree.ofBin (BinaryTree.node value l r) = (Nock.BTree.ofBin l).node (Nock.BTree.ofBin r)

@[simp]

theorem Nock.BTree.ofBin_toBin (t : BTree) : ofBin t.toBin = t

@[simp]

theorem Nock.BTree.toBin_ofBin (t : BinaryTree Unit) : (ofBin t).toBin = t

theorem Nock.BTree.size_eq (t : BTree) : t.size = 2 * t.toBin.numNodes + 1

Under the shape isomorphism, BTree.size is 2·numNodes + 1: a proper binary tree with λ internal (Mathlib) nodes has 2λ+1 total nodes (Lem:pbt_size, main.tex:333).

noncomputable def Nock.BTree.dyckWordsOfLen (lam : ℕ) : Finset (List Bool)

|L^{2λ}_dk| as a finset (main.tex:337–341). The Dyck words of length 2λ, obtained as the image of Mathlib's treesOfNumNodesEq λ under encode ∘ ofBin.

Equations

• One or more equations did not get rendered due to their size.

theorem Nock.BTree.mem_dyckWordsOfLen {lam : ℕ} {w : List Bool} : w ∈ dyckWordsOfLen lam ↔ Dyck w ∧ w.length = 2 * lam

A word lies in dyckWordsOfLen λ iff it is a Dyck word of length 2λ — i.e. this finset is exactly the paper's L^{2λ}_dk.

theorem Nock.BTree.dyckWordsOfLen_card (lam : ℕ) : (dyckWordsOfLen lam).card = catalan lam

Lem:optimal_dyck (main.tex:340–342). |L^{2λ}_dk| = C_λ.