wellFormed_C
plain-language theorem explainer
Configuration C, the loom encoding of “some door locks every key” conjoined with “every door opens every key,” is well formed: every loop is reduced and the frame generator is present. Certificate and separation readers cite this to know C passes the kernel checker before any reading or gauge check. Proof is a one-line wrapper: C is the weave of a grammar expression, and every weave is well formed.
Claim. The configuration $C$ obtained by weaving the conjunction of “some door locks every key” with “every door opens every key” under the second codebook satisfies $\mathrm{wellFormed}(C)=\mathrm{true}$: every loop is a reduced word and the frame loop is present.
background
In the Loom, quantified door/key formulas are encoded as configurations: finite lists of loops (words in a free group with a distinguished frame generator). The total checker declares an utterance well formed when every loop is reduced and the frame loop appears; both conditions are decidable in linear time.
This module’s separation suite studies content patterns that agree under shallow readings but disagree under deeper ones. Witness C is the conjunction of “some door locks every key” with “every door opens every key.” Under codebook two it weaves to the concrete certificate configuration C. Weaver soundness states that everything the grammar produces is well formed, so the checker never rejects an honest utterance.
proof idea
One-line wrapper. Rewrite via the identity that weaving witness C under codebook two recovers configuration C, then apply weaver soundness: every woven expression is well formed.
why it matters
Pins the third certificate configuration in the Loom separation suite as a legitimate kernel input. The module’s main results show that depth-one and abelianised readings conflate the A/B pair while the commutator reading and the full gauge orbit (order 96 times basepoint choice, all 48 automorphisms) separate them. C is a parallel quantified pattern that must also clear well-formedness before any reading or invariant comparison. No downstream uses are wired yet, so this is a leaf certificate fact rather than an intermediate lemma in the A/B separation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.