cbData
plain-language theorem explainer
Integer codebook mapping the four Loom generators door, key, opens, locks to −1, 3, 4, 5 in that fixed name order. Separation proofs cite it as the free convention under which no length statistic distinguishes the witness pair. The value is emitted certificate data, not a derived theorem: a four-element list the separation module indexes by name.
Claim. The codebook is the ordered integer assignment $\mathrm{door}\mapsto -1$, $\mathrm{key}\mapsto 3$, $\mathrm{opens}\mapsto 4$, $\mathrm{locks}\mapsto 5$, written as the list $[-1,3,4,5]$. Under this assignment no length statistic separates the measured witness pair.
background
The Loom certificate module stores machine-emitted data that the separation proofs treat as trusted input. A codebook is an assignment of integer labels to the four free generators of the utterance language (door, key, opens, locks). Which assignment is used is a free convention: an invariance result on substitution configs shows that gauge-equivalent codebooks yield the same separation verdict.
The module doc records that exhaustive search chose this particular map so that both members of the flagship witness pair cost 142 acts with the same per-loop multiset $[4,8,8,16,18,40,48]$. Depth-one and abelianised readings of the pair are identical; only the depth-two reading differs. A second pair under a different codebook appears later in the same file.
Upstream edges into foundation material (circle winding, Clifford bridge, forcing chain $D=3$ and eight-tick) are incidental name collisions in the dependency graph, not mathematical inputs to this list.
proof idea
Pure data definition: the body is the literal four-element integer list $[-1, 3, 4, 5]$. No tactic, no lemma application. The list is regenerated by the Loom emitter from certificate.json whenever the encoder or search changes; it is not hand-edited.
why it matters
Downstream, the separation module aliases this list as its working codebook and uses it to interpret the two configurations under test. The doc on that alias stresses that the search deliberately chose a codebook under which length statistics fail to separate the pair, so the kernel check is harder rather than easier.
In the Loom story this is the measured certificate that makes separation kernel-checkable: identical depth-one readings, identical abelianised readings, and a depth-two discrepancy that Lean can decide. It does not itself touch the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder; it is infrastructure for the Loom separation claim that two utterances are gauge-indistinguishable at shallow readings yet distinguishable at depth two.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.