wellFormed
plain-language theorem explainer
Total Boolean checker for Loom utterances: a finite list of closed walks is well formed exactly when every word is freely reduced and the distinguished frame loop is present. Certificate authors, the weaver soundness proof, and the separation witnesses all cite it. The body is a one-line conjunction of two linear-time list predicates.
Claim. For a configuration $c$ (a finite list of words in the free group on the five Loom generators), return true if and only if every word of $c$ is freely reduced and $c$ contains the singleton word consisting of the frame generator.
background
Loom is a certificate language for finished recognition histories. On the eight-state, three-axis window fixed by the forcing chain, closed walks up to homotopy form a free group of rank five, so a finished utterance is a finite list of words in five signed generators sharing one basepoint.
A configuration is exactly that list. Content is read up to free reduction (spelling is not content) and up to simultaneous conjugation of every loop (basepoint is not content). The module supplies a total checker, a computable SL(2, Z/3Z) invariant blind to those two operations, and nothing else: no model, no search.
The checker only asks two decidable questions: every loop is a reduced word, and the distinguished frame loop appears in the list. Both run in linear time in the total length of the utterance.
proof idea
Pure definition, not a derived theorem. Evaluate the Boolean conjunction of (i) List.all of the free-reduction predicate on every word of the configuration and (ii) list membership of the singleton frame-generator word. No lemmas are applied; the body is the specification.
why it matters
This is the gate every honest Loom object must pass. Downstream, the specification theorem shows every framed, freely reduced configuration is accepted, so the verdict is a fact about the words rather than a wish. Weaver soundness reduces to that fact: everything the grammar produces is well formed. The four separation witnesses (A through D) each discharge the checker before their invariants are compared, so the separation argument never mixes ill-formed input with genuine collisions.
In the broader Recognition setting the checker sits on the eight-tick, rank-five free group fixed by T7 and the window Euler characteristic. It carries no physics model; it only certifies that a finished object is eligible for the trace-and-commutator invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.