door
plain-language theorem explainer
The name “door” is fixed as codebook index 0 among the four shared atoms (door, key, opens, locks). Separation and certificate modules cite it whenever they build quantified door/key formulas or bind the blinding codebook. The body is a one-line Nat constant.
Claim. The shared name “door” is assigned the codebook index $0\in\mathbb{N}$. Together with the indices for “key”, “opens”, and “locks”, it labels the four atoms used by the Loom separation witnesses.
background
The Loom separation module compares two first-order patterns that look identical under length and multiset statistics: (A) every door has some key that opens it, and one master key locks every door; (B) the dual security-hole pattern with opens/locks swapped in quantifier power. Both are built from the same four atoms.
Those atoms are not strings in the kernel; they are Nat codebook indices. The module doc states that the codebook was chosen by exhaustive search so both witnesses cost the same number of one-bit acts with the same per-loop length multiset, so counting alone cannot separate them.
Certificate data records the chosen codebook in name order [door, key, opens, locks]. Index 0 is therefore the conventional slot for “door” in every quantified Expr and in the Config lists that the weaver replays.
proof idea
Pure definition: the constant natural number 0. No proof obligations, lemmas, or tactics.
why it matters
Every quantified separation formula indexes the door binder through this constant: everyDoorOpensEveryKey, everyDoorLocksEveryKey, everyDoorSomeKeyOpens, everyDoorSomeKeyLocks, and the dual master-key patterns. CertificateData.cbData and cbData2 place door first in the blinding codebooks [-1,3,4,5] and [1,3,-4,5]; cfgA and cfgC embed the same index in the loop Configs that weave_witnessA/B must reproduce letter-for-letter.
Without a fixed Nat atom the depth-one and abelianised blindness theorems, the commutator separation, and the 48-automorphism gauge check (no_gauge_image_of_A_is_B) would have nothing stable to quantify over. The definition is scaffolding for the claim that two meanings remain distinct after the full recognition-window gauge group is quotiented out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.