1 EML Registry: Tamari Lattice Contraction
1.1 Core Types
The type of binary trees representing configurations in the Tamari lattice. A tree is either a Leaf (empty configuration) or a Node \(t_1\ t_2\) (composition of two sub-configurations).
The number of internal nodes in a tree, used as the lattice index \(n\) in \(T_n\).
The primitive non-associative rewrite rule: \((a \bullet b) \bullet c \to a \bullet (b \bullet c)\). This is the coupling signature for choice resolution, lifted through subtrees.
The reflexive-transitive closure of contracts_one. Represents an audit trail of choice resolutions with monotonic provenance.
The minimum element of the Tamari lattice — the equilibrium attractor. Defined as \(\mathsf{rightComb}(0) = \mathsf{Leaf}\) and \(\mathsf{rightComb}(n+1) = \mathsf{Node}(\mathsf{Leaf},\ \mathsf{rightComb}(n))\).
1.2 Lifting Lemmas
If \(t \to t'\) then \(\mathsf{Node}(t,\ r) \to \mathsf{Node}(t',\ r)\). Choice resolution in the left subtree propagates to the whole composition.
If \(r \to r'\) then \(\mathsf{Node}(l,\ r) \to \mathsf{Node}(l,\ r')\). Choice resolution in the right subtree propagates to the whole composition.
If \(s \to t\) and \(t \to u\) then \(s \to u\). Audit trails concatenate monotonically.
1.3 Size Invariants
Rotation rewrites the tree depth but does not change the number of internal nodes.
Contraction paths preserve tree size, establishing that the Tamari lattice \(T_n\) is graded by node count \(n\).
1.4 Main Contraction Theorem
For any \(a, b : \mathbb {N}\),
The equilibrium attractor is closed under non-associative composition.
For any tree \(t : \mathsf{EMLTree}\),
Every configuration has a valid evolution path to the equilibrium attractor indexed by its size.
1.5 Router and Registry
A bounded natural number \(\mathsf{Fin}(n)\) serving as a neural binding address.
An injective mapping from router indices to EML trees. This is the cortex-registry interface where neural computation meets formal grammar.
1.6 Witness-Skeptic Game
A proof-carrying audit trail \(\langle source,\ target,\ proof \rangle \) showing that a tree reaches its equilibrium.
Issues a CortexCertificate for any tree \(t\), certifying that \(t \to \mathsf{rightComb}(t.\mathsf{size})\). This is the quench witness in the Witness-Skeptic game.