wellFormed_D
plain-language theorem explainer
Configuration D, packing the claim that some door opens every key and every key opens every door, is a well-formed Loom utterance: every loop is reduced and the frame loop is present. Separation and certificate work cite it to know the kernel accepts D without rejection. The proof is a one-line rewrite through the weaver equality, then soundness of weave.
Claim. The Loom configuration $D$ (encoding "some door opens every key, and every key opens every door") satisfies the well-formedness checker: every loop is a reduced word and the frame generator loop is present, so $\mathrm{wellFormed}(D)=\mathrm{true}$.
background
The Loom kernel treats an utterance as a configuration: a list of loops (words in the recognition generators). The total checker wellFormed accepts a configuration exactly when every loop is reduced and the distinguished frame loop is present; both tests are decidable in linear time.
The grammar side builds configurations by weaving an expression tree through a codebook. Soundness of that weaver states that every woven utterance is well formed, so an honest encoder never fails the checker. Configuration D is the concrete packing of the conjunction "some door opens every key" with "every door locks every key," obtained by weaving a fixed codebook against the corresponding expression tree.
This module's setting is the separation witness: two door/key formulas that agree under every depth-one and abelianised reading, cost the same under the codebook, yet are distinguished by the commutator reading and by the full gauge orbit. D sits among the certificate configurations used in that comparison.
proof idea
One-line wrapper. Rewrite the goal along the decided equality that weaving the second codebook on the D expression tree recovers configuration D. The goal becomes well-formedness of a woven utterance, which is immediate from the weaver soundness lemma applied to that codebook and expression.
why it matters
Closes the kernel-acceptance obligation for configuration D inside the Loom separation stack. The module's larger claim is that two content-identical-looking door/key formulas are gauge-inequivalent meanings: depth-one and abelianised readings are blind, the commutator reading separates them, and no automorphism image of A is B. Having D well formed means the certificate data for the dual packing (some door opens every key, every key opens every door) is honest input to those comparisons rather than rejected noise.
No downstream theorem currently depends on this lemma in the graph, so it is a local certificate fact rather than a forcing-chain step. It does not touch T0–T8, the Recognition Composition Law, or the mass ladder; it is Loom infrastructure for meaning separation under gauge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.