witnessA
plain-language theorem explainer
Safe separation witness A: every door has some key that opens it, and one master key locks every door. Built as the unordered conjunction of those two quantified Loom formulas over the shared codebook. Cited by the weaver match, well-formedness check, and the gauge-separation theorem that no image of A equals B. Pure inductive term; no proof work.
Claim. Let $A$ be the Loom expression $\bigl(\forall d\,\exists k\,\mathrm{Opens}(k,d)\bigr)\land\bigl(\exists k\,\forall d\,\mathrm{Locks}(k,d)\bigr)$, formed as the unordered conjunction of the two quantified atoms over the shared codebook names for door, key, opens, and locks.
background
The Loom separation module builds two content formulas that agree under every depth-one and abelianised reading, yet are inequivalent under the full gauge group of the recognition window. Formula A is the safe policy; formula B is the dual security hole. They use the same two relations and the same two quantifier patterns, differing only in which relation receives universal power.
Content lives in the Loom grammar Expr: atoms are codebook-indexed relations on role fillers (optionally denied), closed under unordered conjunction and under quantifiers over shared names (universal when the flag is true). The four names here are fixed indices: door $=0$, key $=1$, opens $=2$, locks $=3$. Upstream, everyDoorSomeKeyOpens is $\forall$ door $\exists$ key Opens(key,door), and someKeyEveryDoorLocks is $\exists$ key $\forall$ door Locks(key,door).
The module doc states the goal: prove the two utterances are letter-for-letter reproductions of the Python encoder, that shallow readings conflate them, that the commutator reading separates them, and that no automorphism image of A is B.
proof idea
One-line definitional wrapper. The term is the inductive constructor for unordered conjunction applied to the two already-defined quantified expressions everyDoorSomeKeyOpens and someKeyEveryDoorLocks. No tactics, no lemmas, no obligations: pure construction in Loom.Grammar.Expr.
why it matters
This is content piece A of the separation witness. It is the input to weave_witnessA, which shows the Lean weaver reproduces the Python encoder utterance letter for letter, so later certificates concern the grammar rather than transcription. It feeds wellFormed_A, which checks that the woven configuration passes the well-formedness checker. It is the left-hand side of witnesses_separated: for every automorphism substitution in the 48-element group, every basepoint word, and every reversal flag, no permutation of the gauge image of woven A equals woven B, even though depth-one and abelianised readings are identical on the pair.
The module frames the strength of the separation in institute terms: the gauge group has order 96 times free basepoint choice, the check covers all 48 automorphism images exactly, and the two invariants differ in one coordinate of twenty-one (the smallest exact margin). The definition itself is scaffolding-free content; the nontrivial work sits in the downstream separation theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.