wellFormed_B
plain-language theorem explainer
Configuration B, the insecure door-key quantifier pattern, is well-formed under the loom grammar. Separation arguments that treat B as a legitimate utterance cite this. The proof rewrites B to the weave of the codebook with witness B, then applies the general fact that every such weave is well-formed.
Claim. The loom configuration associated to witness B is well-formed: $\mathrm{wellFormed}(\mathrm{cfg}_B)=\mathsf{true}$.
background
The Loom.Separation module builds two short utterances over a shared door-key vocabulary. Pattern A says every door has some key that opens it and one master key locks every door. Pattern B swaps the universal power: every door has some key that locks it and one master key opens every door. A is secure; B is a security hole. They use the same two relations and the same quantifier shapes, so length and multiset counts cannot separate them.
Both utterances are produced by a weaver from a fixed codebook and a ground witness. The module first proves that the Lean weaver reproduces the Python encoder output letter for letter (weave_witnessA, weave_witnessB), so later reasoning is about the grammar, not opaque data. Well-formedness is the kernel check that a configuration is a legal weave under that grammar.
This theorem is the B-side half of that check: once B is known to equal the weave of the codebook with witness B, well-formedness follows from the general weave lemma.
proof idea
Term-mode, two steps. Rewrite the goal with the equality that identifies configuration B with the weave of the codebook and witness B. Discharge the rewritten goal by the general lemma that every weave of that codebook with a witness is well-formed. No case split and no arithmetic.
why it matters
Without well-formedness of B, the separation story collapses: one could dismiss B as ill-formed junk rather than a genuine meaning that depth-one and abelianised readings conflate with A. Together with the A-side twin, this pins both utterances inside the grammar so that depth_one_is_blind, abelianised_is_blind, depth_two_separates, and the full gauge non-image result (no_gauge_image_of_A_is_B) can treat them as peer configurations.
The module frames the strength of the separation in institute terms: the gauge group has order 96 times free basepoint choice, all 48 automorphism images are covered exactly, and the two invariants differ in one coordinate of twenty-one (the smallest exact margin). This lemma is a load-bearing well-formedness gate on that path. No downstream consumers are recorded yet in the graph; it is infrastructure for the separation package itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.