cb2
plain-language theorem explainer
The second separation codebook is the fixed four-integer labelling [1, 3, −4, 5] that attaches signed generators to the shared names door and key. Anyone citing the C/D witness pair (some-door-locks-every-key versus some-door-opens-every-key) uses this codebook. It is a one-line alias of the certificate data constant, so the weaver and gauge checks inherit a concrete, machine-checked labelling.
Claim. Let the second codebook be the list of signed generator attachments $[1, 3, -4, 5]$. This is the shared labelling of the bound names used by the second separation witness pair.
background
In the Loom separation module the content under study is two pairs of quantified claims about doors and keys. The flagship pair A/B is already separated under a first codebook; the second pair C/D asks the same quantifier question in a form that also defeats readings carrying parent-to-child parse labels.
A codebook is simply a list of integers: which signed generator each shared name is attached to. Sender and receiver must share it. It is not pure gauge; the automorphism group of the recognition window does not act transitively on labellings, so a codebook retains a residue of real choice.
The certificate data supply the concrete list for the second witness: the codebook that also equalises the per-loop length multiset, so both utterances cost 88 acts with identical loop-length multisets. Act-count and amplitude readings separate the pair under none of the 384 codebooks; this labelling separates it under every one of them.
proof idea
One-line definitional alias: the local name is bound exactly to the certificate-data constant that holds the list $[1, 3, -4, 5]$. No proof obligations; the type is the Grammar abbreviation for a list of integers.
why it matters
Every subsequent check for the second witness is parameterised by this codebook. The weaver equalities that reproduce the Python encoder output letter-for-letter, the well-formedness of the two configurations, and the gauge-orbit separation theorem all instantiate the weaver and the gauge image at this labelling. Downstream, the separation theorem states that no automorphism, basepoint move, reversal, or loop reordering sends the weave of C to the weave of D. That is the content-level claim the module exists to certify: the two formulas receive utterances no gauge transformation identifies, even though every depth-one reading agrees and the labelled-tree multiset is identical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.