locksDoorKey
plain-language theorem explainer
Atomic positive formula locks(door, key) in the Loom grammar, with codebook indices door=0, key=1, locks=3 and denial off. Separation witnesses cite it as the ground relation under nested quantifiers. Defined by a one-line atom constructor.
Claim. The ground atomic formula $\mathrm{locks}(\mathrm{door},\mathrm{key})$ as a Loom grammar expression: predicate index $3$, role fillers $[0,1]$ in order, denial flag false.
background
The Loom separation module builds two quantified utterances over a shared door/key vocabulary that agree on every depth-one and abelianised reading, yet differ under the commutator reading and under the full gauge group of the recognition window. Content is written in Grammar.Expr: atoms are a predicate index, a list of role-filler name indices, and a denial bit; conjunction and quantifiers (universal when the flag is true) close the language. Names are codebook indices, never free strings.
Here the four shared names are fixed: door $= 0$, key $= 1$, and locks $= 3$ (opens is the other binary relation). The codebook itself was chosen by exhaustive search so that length and multiset statistics cannot separate the pair; that choice is a free convention once gauge invariance of the invariant is in hand. The expression tree is the native object the weaver and the kernel both consume.
proof idea
Pure definition: apply the grammar constructor atom to predicate locks, argument list [door, key], and denial false. No lemmas, no tactics.
why it matters
Ground atom for the locks side of the separation pair. Downstream, someDoorLocksEveryKey wraps it as $\exists,\mathrm{door},\forall,\mathrm{key},\mathrm{locks}(\mathrm{door},\mathrm{key})$, and everyDoorLocksEveryKey as $\forall,\mathrm{door},\forall,\mathrm{key},\mathrm{locks}(\mathrm{door},\mathrm{key})$. Those quantified forms enter witness B (every door has some locking key, and one master key opens every door), the security-hole pattern that counting and depth-one readings conflate with witness A. The module then shows depth-two commutator separation and that no image under the order-96 gauge action (48 automorphisms, basepoint moves, reversal, respelling, loop reorder) sends A to B. Without this atom the quantified witnesses have nothing to quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.