cbData2
plain-language theorem explainer
Integer codebook [1, 3, −4, 5] assigning generators door, key, opens, locks for the second Loom witness pair. Separation proofs and the stronger cfgC/cfgD certificate cite it as the encoding that defeats parent-to-child label readings. Pure data definition emitted from the measured certificate; no proof obligations.
Claim. The second witness codebook is the integer list $[1, 3, -4, 5]$, assigning values door $\mapsto 1$, key $\mapsto 3$, opens $\mapsto -4$, locks $\mapsto 5$ to the four shared generator names.
background
The Loom certificate module stores measured search output as Lean data: free-group homomorphisms into $\mathrm{SL}_2(\mathbb{Z}/3\mathbb{Z})$, automorphism tables for the cube group $Q_3$, and encoder configurations. Codebooks map the four shared names (door, key, opens, locks) to integer labels so that utterances become words in a free group of rank five.
The first codebook used ${-1, 3, 4, 5}$. This second list ${1, 3, -4, 5}$ is the encoder choice for the stronger pair (cfgC, cfgD). Both members cost 88 acts with the same per-loop multiset, and they remain conflated even under readings that carry parent-to-child labels; only an explicit homomorphism separates them.
Indices door $= 0$, key $= 1$, opens $= 2$ (and locks as the fourth slot) fix the order of the list entries. Provenance of the tables is trusted from the Python configuration; Lean checks only that each table satisfies the decidable Table.ok predicate.
proof idea
Definitional constant: the body is the literal list [1, 3, -4, 5]. No tactics, no lemmas, no reduction. Downstream code wraps it as a Codebook value.
why it matters
Feeds cb2 in the separation module, which packages the whole second witness as a content-level statement: the two formulas receive utterances that no gauge transformation identifies, even though every depth-one reading agrees. That is the stronger half of the measured separation claim in the module doc: the flagship pair is separated only by a depth-two syntactic reading, while this pair is conflated by that reading too and is separated by an explicit model.
In the Loom story this data makes kernel-checkable the claim that length statistics and shallow readings cannot tell the witnesses apart, while a concrete homomorphism can. It sits downstream of the cube automorphism tables and the base free-group homomorphism; it does not itself touch the T0–T8 forcing chain or the J-cost calculus, but it is the concrete certificate that the recognition-side separation argument consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.