opensKeyDoor
plain-language theorem explainer
Atomic ground fact that the key opens the door, written as a Loom grammar atom with predicate index opens, role fillers key then door, and denial off. Separation witnesses cite it as the open-relation body under both quantifier orders. The body is a single constructor application of Expr.atom.
Claim. The ground atom asserting that codebook name $\mathrm{key}$ stands in the $\mathrm{opens}$ relation to codebook name $\mathrm{door}$, with the denial flag false: $\mathrm{atom}(\mathrm{opens},[\mathrm{key},\mathrm{door}],\bot)$.
background
Module Loom.Separation builds a kernel-checked separation witness: two quantified English-style claims that share the same multiset of ground facts and the same one-bit act costs, yet mean different things under depth-two (commutator) reading and under the full gauge group of the recognition window.
Content is Grammar.Expr: atoms are a predicate index, an ordered list of role-filler name indices, and a denial bit; conjunction and quantifiers (universal when the flag is true) build the rest. Names are shared codebook indices, not per-claim strings. Locally the four names include door := 0, key := 1, and the open-relation index opens := 2.
This definition is the undenied open atom on those two fillers. Upstream Expr (Loom grammar) is the only type; the certified-analytic Expr in the depends list is a different inductive and is not the carrier here.
proof idea
Definitional one-liner, not a proof. Applies the Expr.atom constructor to predicate opens, argument list [key, door], and denied := false. No lemmas, rewrites, or tactics.
why it matters
Supplies the open-relation body for both quantifier patterns that form half of witness A: everyDoorSomeKeyOpens (every door has some key that opens it) and someKeyEveryDoorOpens (one master key opens every door). Those feed the weave, depth-one blindness, depth-two separation, and no-gauge-image theorems that show A and B are distinct meanings, not two spellings of one fact multiset.
In the module's terms, counting and abelianised readings conflate A and B; the commutator reading and the order-96 gauge quotient separate them by one coordinate of twenty-one. This atom is the open half of that pair; the lock atom is the dual. It is scaffolding for the separation story, not a physics constant claim (no direct T5–T8 or RCL content).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.