everyDoorOpensEveryKey
plain-language theorem explainer
Nested universal quantification: every door opens every key, as a Loom grammar expression tree. Separation and witness constructions cite it as one conjunct of witness C. The body is a pure definitional nesting of two universal quantifiers over the opens atom.
Claim. The Loom expression $\forall\,\mathrm{door}\,\forall\,\mathrm{key}\,\mathrm{opens}(\mathrm{door},\mathrm{key})$, built as two nested universal quantifiers over the shared codebook names for door and key applied to the non-denied opens atom.
background
The Loom grammar represents content as finite expression trees: atoms (a predicate index, role-filler name indices, and a denial flag), unordered conjunction, and quantifiers over shared codebook names (universal when the flag is true). Names are indices into one shared codebook, so nothing is anonymous or claim-local.
In this module the four shared names are fixed indices (door $= 0$, key $= 1$, and the opens/locks predicates). The atom opensDoorKey is the ground relation opens(door, key) with denial false. The module's separation witnesses compare two quantifier patterns over opens versus locks: one is a legitimate access story, the other a security hole. Counting and depth-one readings cannot tell them apart; depth-two (commutator) readings and the full gauge orbit can.
This declaration is only the pure universal-universal opens half of that vocabulary, not yet conjoined or woven.
proof idea
Definitional one-liner. It builds an Expr by nesting two universal quantifiers (flag true) over the door and key name indices, with body the already-defined opens atom on those two roles. No tactic proof and no lemma applications.
why it matters
Feeds witnessC, which conjoins "some door locks every key" with this universal opens claim. That witness sits in the Loom separation suite whose point is that two utterances can share the same multiset of ground facts, the same one-bit act counts, and the same per-loop length multiset, yet differ in meaning under depth-two and gauge-invariant readings.
The module proves weave fidelity, depth-one and abelianised blindness on the A/B pair, depth-two separation, and that no image of A under the recognition-window automorphism group (order-48 auts, basepoint moves, reversal, respelling, loop reorder) equals B. This definition supplies one atomic quantified clause those witnesses assemble. It is scaffolding vocabulary for the separation, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.