wellFormed_A
plain-language theorem explainer
Utterance A of the Loom separation pair is well formed: every loop is reduced and the frame loop is present. Anyone citing the kernel-checked separation needs this certificate before comparing readings or gauge orbits. The proof is a one-line wrapper: rewrite A as the weave of its expression, then apply grammar soundness.
Claim. The Loom configuration for utterance A (every door has some key that opens it, and one master key locks every door) satisfies the total checker: every loop is a reduced word and the frame loop is present, so $\mathrm{wellFormed}(A)=\mathrm{true}$.
background
The Loom separation module exhibits two utterances that agree on every depth-one and abelianised reading, and on all length multisets under a carefully chosen codebook, yet differ under the commutator (depth-two) reading and under the full gauge group of the recognition window. Utterance A is the safe reading: keys open doors one at a time, and one master key locks every door. Utterance B swaps the universal power and is a security hole.
A configuration is well formed when every loop is a reduced word and the frame generator loop is present; both checks are decidable in linear time. The weaver turns a codebook and an abstract expression into a concrete configuration. Soundness of the weaver states that every woven utterance is well formed, so the checker never rejects an honest grammar product.
The certificate data supply a fixed codebook (chosen so length statistics cannot separate the pair) and the concrete loop list for A. A prior decide-proof shows the weaver reproduces that list letter for letter from the expression for A.
proof idea
One-line wrapper. Rewrite the goal along the identity that weaving the codebook on the expression for A yields exactly the certificate configuration for A. The goal becomes well-formedness of a woven utterance, which is discharged by the grammar soundness lemma (everything the weaver produces is well formed).
why it matters
This is the first kernel check in the separation witness package: both utterances must pass the checker before any claim that depth-one readings are blind, that depth two separates, or that no gauge image of A is B. The module doc requires that nothing below rests on opaque data; together with the matching weave identity, this theorem pins A to the grammar rather than to a transcribed bitstring.
No downstream theorem currently depends on this declaration by name, but the narrative of the module treats well-formedness of A and B as the entry ticket to the nontrivial separation (identical carriers at depth one, distinct commutator readings, and a full 48-automorphism non-identification). It does not itself touch the forcing chain T0–T8; it is Loom infrastructure for meaning separation under recognition-window gauge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.