everyDoorSomeKeyOpens
plain-language theorem explainer
Encodes the quantified claim that every door is opened by at least one key, as a Loom expression tree over shared codebook names. Anyone assembling the safe separation witness cites it as the first conjunct. The body is a pure constructor: universal over door, existential over key, applied to the opens atom.
Claim. The Loom expression $\forall d\,\exists k\,\mathrm{opens}(k,d)$, where $d$ and $k$ are the shared codebook indices for door and key, and $\mathrm{opens}$ is the binary opens-relation atom (not denied).
background
The Loom grammar accepts finite expression trees whose leaves are atoms over a shared codebook: predicate index, argument name indices, and a denial flag. Quantifiers are written .quant univ name body, with univ = true for $\forall$ and false for $\exists$. Names are never anonymous; door, key, and opens are fixed Nat indices (0, 1, 2).
The module builds two security-flavoured utterances that share the same ground multiset and the same one-bit act cost, yet differ in meaning. One pattern is safe (keys open doors one at a time; one master key locks everything). The other is a security hole (one master key opens every door). This definition is the first half of the safe pattern: every door has some key that opens it.
Upstream, opensKeyDoor is the ground atom opens(key, door) with denial false. The present definition wraps that atom in nested quantifiers.
proof idea
Not a proof: a one-line def that builds an Expr term. Outer constructor is universal quantification over the door name; inner is existential quantification over the key name; matrix is the already-defined opens atom on [key, door]. No lemmas are applied.
why it matters
Feeds directly into witnessA, the safe separation witness: the conjunction of this formula with "some key locks every door." That witness is what the module contrasts with the unsafe dual (master key opens everything). The pair is the content on which depth-one and abelianised readings are blind, while the commutator reading and the full gauge-orbit check separate them. Without this conjunct, the safe side of the Loom separation has no formal utterance. It is scaffolding for meaning, not a forcing-chain step (T0–T8); its role is local to the Loom grammar and the kernel-checked separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.