cfgB
plain-language theorem explainer
Literal second witness of the Loom discovery pair: seven integer words encoding the sentence “every door has some key that locks it, and one master key opens every door” under the fixed codebook door↦−1, key↦3, opens↦4, locks↦5. Downstream classical-source and decoy theorems cite it as the partner of cfgA. The body is emitted data, not a derived proof.
Claim. Let $\mathrm{cfgB}$ be the fixed list of seven integer words $$[[2],[-1],[-1,-3,1],[-1,-3,5,3,-1,5,3,1],[-3],[-3,-1,3],[-3,-1,4,3,-1,4,1,3]],$$ the encoder image of the English witness “every door has some key that locks it, and one master key opens every door” under the codebook $\{\mathrm{door}\mapsto -1,\,\mathrm{key}\mapsto 3,\,\mathrm{opens}\mapsto 4,\,\mathrm{locks}\mapsto 5\}$. Together with its partner configuration it forms the discovery pair of equal classical cost $142$ and identical depth-one and abelianised bags.
background
The Loom certificate module stores machine-emitted Lean data for a measured separation of two natural-language witnesses. A configuration here is a list of integer words (loops) in the free group on five generators; the integers are codebook labels, not abstract group elements. The discovery pair uses the codebook door↦−1, key↦3, opens↦4, locks↦5, chosen by exhaustive search so that no length statistic separates the two members: both cost 142 acts with the same per-loop multiset [4, 8, 8, 16, 18, 40, 48].
The module also records a base homomorphism into SL(2, Z/3Z) and forty-eight automorphism tables for the cube group Q3. Only the provenance of those tables is trusted; Table.ok is decidable and rechecked in the separation module. Depth-one and abelianised readings of the pair are identical ([0,0,2,2,2,2,2] and the corresponding abelian bag); only the depth-two reading differs. A second, stronger pair (cfgC, cfgD) appears later under a different codebook.
proof idea
Pure data definition. The right-hand side is a concrete nested list literal produced by Loom/lean/emit_lean_data.py from certificate.json; there is no tactic proof, no lemma application, and no algebraic reduction. Lean simply binds the name to that value of type Config.
why it matters
cfgB is the second half of the discovery pair that makes the Loom separation kernel-checkable. Parent results in ClassicalSourceProjection use it to prove: depth-one sources of cfgA and cfgB agree; abelianised sources agree; yet the depth-two reading separates them. The composite certificate classicalEqual_recognitionUnequal_cfgAB packages those three facts. Decoy theorems instantiate the same pair to show that any reading factoring through the depth-one bag or the abelian bag is blind on discovery. Continuum residual arguments also cite the pair when arguing that finite exclusion does not earn promotion. In the broader Recognition stack this supplies a concrete, machine-checked witness that classical (depth-one / abelian) projections lose information that the recognition depth-two reading retains, without relying on the forcing chain T0–T8 or the mass ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.