Codebook
plain-language theorem explainer
A codebook is a finite list of signed integers assigning each shared name to a generator of the free group. Sender and receiver must agree on it before any utterance is woven. It is not pure gauge: orbit counts show at least fifteen inequivalent labellings survive relabelling. Every production rule in the weaver reads letters through this list.
Claim. A codebook is a list of integers $c = (c_0, c_1, \ldots)$ in which the entry $c_n$ is the signed generator attached to shared name $n$. Missing indices default to $0$. This list is the entire pre-shared labelling that sender and receiver must hold in common.
background
In the Loom grammar, content is an inductive expression (Expr) and an utterance is a configuration of freely reduced closed walks. The weaver turns content into such a configuration by five production rules forced by the algebra of the free group: ordered product for relations, inversion for denial, multiset union for conjunction, and binder-loop conjugation for quantifiers, all framed by the recognition window.
Names that appear in atoms and binders are not themselves generators. They are indices into a pre-shared list of signed integers. That list is the codebook. Looking up name $n$ yields the letter that will be written into the walk; the default for an out-of-range index is zero.
The module setting is deliberately total: every expression weaves, every woven configuration is well-formed, and spelling is reduced away so that only content remains. The codebook is the one piece of data that is not derived from the expression itself.
proof idea
Pure abbreviation: Codebook is identified with List Int. There is no proof obligation. Downstream definitions such as letter lookup simply read the $n$-th entry with default $0$, and the five production rules of the body weaver thread that lookup through atoms, conjunctions, and quantified binders.
why it matters
Every path from content to utterance depends on a codebook. Letter lookup, the body weaver, the framed weaver, soundness of weaving against the well-formedness checker, invariance of the woven invariant under free reduction, and the depth-one trace identity for quantified bodies all take a codebook as an argument. Separation lemmas in the sibling module instantiate concrete codebooks when exhibiting distinct utterances.
The doc-comment records a non-gauge fact: the attachment of names to generators is not absorbed by the residual gauge group. Orbit-counting results show that fourteen orbits are insufficient and fifteen suffice, so a codebook carries irreducible choice. In the broader Loom picture this is the shared dictionary that makes recognition of closed walks into communication rather than pure geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.