opensDoorKey
plain-language theorem explainer
Atomic Loom formula asserting the opens relation on the door and key roles, undenied. It is the ground atom under the quantified door/key patterns that build the two separation witnesses. Anyone citing the A/B door-key separation uses this as the shared relational core. The body is a one-line grammar constructor.
Claim. The undenied atomic formula $\mathrm{opens}(\mathrm{door},\mathrm{key})$, where $\mathrm{door}$, $\mathrm{key}$, and $\mathrm{opens}$ are fixed codebook indices $0$, $1$, and $2$.
background
The Loom separation module compares two quantified door/key stories that share the same multiset of ground facts and the same one-bit act costs, yet differ in meaning once depth-two (commutator) structure is read. Content is written in the Loom grammar: an expression is either an atom (predicate index, role-filler indices, denial flag), a conjunction, or a quantifier over a shared name.
The four shared names are codebook indices. Here door is $0$, key is $1$, and opens is $2$. The atom constructor packages a relation applied to role fillers in role order, with a Boolean denial flag. This definition is the undenied opens-atom on those two roles; sibling atoms (locks, swapped argument order) sit beside it for the dual patterns.
proof idea
Pure definition: apply the Loom atom constructor to predicate index opens, argument list [door, key], and denial flag false. No lemmas, no tactics.
why it matters
This atom is the relational core of the opening half of the separation pair. Downstream, someDoorOpensEveryKey and everyDoorOpensEveryKey wrap it in existential/universal quantifiers over door and key, feeding the weave of witness A (every door has some key that opens it, with a master key that locks every door) versus the security-hole dual B.
The module's point is that shallow readings (depth-one loop reading, abelianised reading) are blind to A versus B, while the commutator reading and the full gauge orbit (48 window automorphisms, basepoint moves, reversals, respellings) separate them. Without a shared undenied opens-atom, those quantified shells would not be comparable under the same codebook and cost multiset.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.