wellFormed_reduceConfig_frame
plain-language theorem explainer
Every framed, freely reduced utterance passes the Loom well-formedness checker. Certificate authors and the grammar soundness proof cite this as the checker's acceptance rule for honest utterances: the verdict never rejects a framed normalisation. The argument unfolds the checker into a Boolean conjunction, uses definitional reduction of the framed list head, and discharges freeness via global reducedness of configuration reduction.
Claim. For every configuration $c$ (a finite list of closed walks sharing one basepoint), the well-formedness checker returns true on the free reduction of the framed configuration obtained by prepending the frame generator to $c$.
background
Loom is a certificate language for finished recognition histories: closed walks on the eight-state, three-axis window forced by the chain. Up to homotopy those walks form a free group of rank five, so an utterance is a finite list of words in five signed generators (a Config), all sharing one basepoint.
Two non-content operations are quotiented out: free reduction (spelling is not content) and simultaneous conjugation of every loop (basepoint is not content). This module supplies a total well-formedness checker, a computable invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ reading loop traces and pairwise commutator traces, and theorems that the invariant is blind to exactly those two operations.
Framing prepends a distinguished frame generator before normalisation. The checker asks that every word be freely reduced and that framing side-conditions hold; the present result is the acceptance half of that specification for framed, reduced inputs.
proof idea
Definitional equality gives that reducing a configuration whose head is already the singleton frame generator leaves that head fixed and reduces the tail: $\mathrm{reduceConfig}([\mathrm{frameGen}]::c)=[\mathrm{frameGen}]::\mathrm{reduceConfig}(c)$.
Rewrite the goal with the definition of the checker and that equality. The checker is a Boolean conjunction; split it with Bool.and_eq_true.
The first conjunct is the List.all reducedness test on the framed list. Unfold List.all_cons and apply all_isReduced_reduceConfig (every word in a reduced configuration is reduced); the frame head is definitionally reduced, so rfl closes.
The second conjunct is discharged by simp (framing side-conditions hold after the same rewrite).
why it matters
This is the checker's positive specification: it never rejects an honest framed utterance, and together with free-reduction lemmas the verdict is a fact about words rather than a wish. Downstream, wellFormed_weave is a one-line application: everything the grammar produces is well formed, so the weaver is sound against the checker. The axiom audit for abelBag (the depth-one multiset of abelianised loops) also lists this theorem among the trusted kernel facts.
In the broader Recognition picture the Loom sits on the eight-tick octave and the rank-five free group of closed walks on the forced window ($E-V+1=5$). The module carries no model and no search; acceptance theorems like this one let a finished certificate be trusted without reconstructing how it was built. Basepoint indifference is no longer a phenomenological load-bearing premise (Loom.BasepointForced removed it from the path); framing-plus-reduction acceptance is the corresponding computational half for the checker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.