someKeyEveryDoorOpens
plain-language theorem explainer
Encodes the claim that a single master key opens every door as a Loom expression: existential over keys, then universal over doors, of the opens atom. Separation and certificate authors cite it as the second conjunct of the unsafe witness B. The body is a direct nesting of two quant constructors on shared codebook names; no proof work.
Claim. The Loom expression for existence of one key that opens every door: $\exists\,k\,\forall\,d\,\mathrm{opens}(k,d)$, built as an existential quantifier over the key name around a universal quantifier over the door name applied to the opens-relation atom.
background
Loom content is a finite expression tree over a shared codebook. Names such as key and door are indices; relations such as opens are atoms. The Grammar Expr inductive type has atoms, unordered conjunction, and a quantifier constructor whose Boolean flag is true for universal and false for existential.
This module builds two separation witnesses that share the same multiset of ground facts and the same one-bit act costs, yet differ in meaning. Piece B is: every door has some key that locks it, and one master key opens every door. Module doc calls B the security hole and A its safe dual (every door has some opening key, and one master key locks every door). The two use the same quantifier patterns and only swap which relation gets universal power.
Upstream Grammar supplies the Expr constructors used here; sibling defs supply the role names key, door and the atom opensKeyDoor.
proof idea
Pure definition, not a proved theorem. The body is the single term that nests .quant false (existential) on key around .quant true (universal) on door applied to opensKeyDoor. No tactics, no lemmas, no obligations.
why it matters
Direct ingredient of witnessB, defined as the conjunction of every-door-some-key-locks with this master-key-opens formula. Downstream doc labels that witness "Unsafe: one master key opens every door." The module then shows the weaver reproduces the Python encoder on B letter for letter, that depth-one and abelianised readings are identical on the A/B pair, that the commutator reading differs, and that no image of A under the 48-window automorphisms (with basepoint moves, reversal, respelling, reordering) equals B. Counting cannot separate them; gauge-invariant depth-two structure can. This is Loom meaning separation at equal cost, not a T0–T8 forcing step, but it shows the recognition grammar can carry inequivalent security claims the shallow readings conflate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.