cb
plain-language theorem explainer
The separation module's fixed codebook maps the four shared names (door, key, opens, locks) to signed generators [-1, 3, 4, 5]. Anyone citing the loom separation witness, weave soundness, or depth-one blindness uses this binding. It is a one-line alias of the certificate-emitted list, not a derived object.
Claim. Let the codebook $C$ be the list of signed generators $[-1, 3, 4, 5]$, attaching the shared names door, key, opens, locks in that order. This is the codebook under which no length statistic separates the two witness utterances.
background
In the Loom grammar, a codebook is a finite list of integers: each shared predicate or argument name is sent to a signed generator. Sender and receiver must already share it. It is not pure gauge; the attachment residue survives the automorphism group of the recognition window (fifteen orbits are needed, fourteen do not suffice).
The separation module compares two quantified meanings that differ only in which binary relation gets universal power: every door has some key that opens it and one master key locks every door, versus the dual security-hole pattern. Both are woven under one codebook so that loop-length multisets and one-bit act counts agree.
Upstream, cbData is exactly that list, taken from the emitted certificate rather than hard-coded by hand, because the blinding search rechooses the labelling whenever the encoder changes. The free-convention fact is that substitution of codebooks leaves the invariant unchanged.
proof idea
One-line definitional alias: the local name is definitionally equal to the certificate list [-1, 3, 4, 5]. No tactics, no lemmas.
why it matters
Every weave, letter lookup, and invariant reduction in the Loom grammar takes a codebook argument; this binding is the concrete one the separation proofs instantiate. Downstream it feeds weave, weaveBody, letterOf, invariant_weave_reduce, trN_weaveBody_quant, wellFormed_weave, and the witness reproduction weave_witnessA.
The module's point is that counting and depth-one readings are blind on the pair while the commutator reading and the full gauge orbit separate them. Fixing the codebook to the search-chosen labelling makes that comparison honest: the test is harder, not easier, because length statistics already match. Without a single shared binding, the letter-for-letter reproduction of the Python encoder's utterances would not type-check against the grammar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.