locksKeyDoor
plain-language theorem explainer
Atomic Loom expression for the positive ground atom “key locks door.” Separation formulas that quantify over keys and doors plug this atom in as their matrix. The definition is a one-line grammar constructor: predicate index locks, role fillers [key, door], denial flag false.
Claim. Let $\mathsf{locksKeyDoor}$ be the atomic expression $\mathsf{locks}(\mathsf{key},\mathsf{door})$ in the Loom grammar, with the denial flag set to false (an affirmed atom, not a negated one).
background
The Loom separation module builds two short quantified utterances that share the same multiset of ground facts and the same one-bit act costs, yet mean different things under a depth-two (commutator) reading. Content is written in Grammar.Expr: atoms are a predicate index, an ordered list of role-filler name indices, and a Boolean denial flag; conjunction and quantifiers (universal when the flag is true) close the language.
Local siblings fix the codebook indices: key and door name the two roles, and locks is the predicate contrasted with opens. The module’s point is that swapping which relation gets universal power turns a safe access pattern into a security hole, while shallow (depth-one or abelianised) readings stay blind to the swap.
Upstream, Expr is the shared inductive type for all such content; nothing anonymous is named, only codebook indices.
proof idea
Pure definition, not a proof. It applies the Expr.atom constructor with predicate locks, argument list [key, door], and denied := false. No lemmas, tactics, or computation.
why it matters
This atom is the matrix of the locking half of the separation pair. Downstream, everyDoorSomeKeyLocks wraps it as $\forall,\mathsf{door},\exists,\mathsf{key},\mathsf{locksKeyDoor}$ and someKeyEveryDoorLocks as $\exists,\mathsf{key},\forall,\mathsf{door},\mathsf{locksKeyDoor}$. Together with the dual opening formulas they assemble witness B (every door has some locking key; one master key opens every door), the security-hole pattern the module separates from the safe witness A.
The separation itself is checked by the kernel: depth-one and abelianised readings conflate A and B, the commutator reading differs, and no gauge image of A equals B. This definition is the shared locking atom those quantified shells need so the comparison is about quantifier–relation placement, not about renaming predicates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.