all_isReduced_reduceConfig
plain-language theorem explainer
After componentwise free reduction of a configuration (a finite list of closed-walk words), every resulting word is freely reduced. Anyone citing the Loom well-formedness checker needs this fact: normalisation lands inside the reduced-word subset rather than merely hoping to. The argument is a short list-map reduction that applies the single-word free-reduction lemma to each image.
Claim. For every configuration $c$ (a finite list of words in the free group of closed recognition walks on the eight-tick window), writing $\mathrm{reduce}(c)$ for the list obtained by freely reducing each word, one has $\mathrm{all}(\mathrm{isReduced},\,\mathrm{reduce}(c))=\mathrm{true}$: every word of $\mathrm{reduce}(c)$ is freely reduced.
background
Loom treats a finished recognition history as a closed walk on the eight-state, three-axis window forced by the T0–T8 chain. Closed walks up to homotopy form a free group of rank $E-V+1=5$, so an utterance is a finite list of words in five signed generators sharing one basepoint. That list type is the configuration.
Spelling is not content: words are identified up to free reduction (cancelling adjacent inverse letters). The predicate isReduced marks words already in free-reduced form; reduceWord computes that form; reduceConfig applies the reduction entrywise to a configuration. The module supplies a total well-formedness checker and a conjugation-blind invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and nothing else: no model, no search.
The single-word lemma that free reduction always yields a reduced word is the immediate upstream fact this statement lifts from words to configurations.
proof idea
Unfold the definition of componentwise reduction and rewrite the Boolean List.all goal as a membership statement via List.all_eq_true and List.mem_map. Any word appearing in the image is the free reduction of some original word $v$; discharge the goal by the single-word lemma that the free reduction of $v$ is reduced. No induction on list length is needed beyond the map characterisation.
why it matters
This is the list-level half of the checker's honesty specification. The immediate parent is wellFormed_reduceConfig_frame, whose doc-comment states that the checker never rejects an honest framed utterance and that its verdict is a fact about the words rather than a wish. That parent splits well-formedness into "every word is reduced" (this theorem, after prepending the frame generator) and a residual frame side-condition.
In the broader Loom story the result closes the free-reduction half of the two non-content operations (spelling and simultaneous conjugation). It does not touch the basepoint/conjugation quotient, which is handled by the trace-class invariant and by Loom.BasepointForced; it only guarantees that the normalisation step the checker relies on really produces reduced words. Framework landmarks in view are the eight-tick octave (T7) and the free group of rank 5 on the forced window, not the mass ladder or $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.