isReduced_reduceWord
plain-language theorem explainer
Free reduction of any word in the five cotree generators is freely reduced. The Loom well-formedness checker cites this so its reduced verdict is a theorem, not a wish. Proof is list induction: empty word is reduced by rfl; the cons case applies the cons-reduction lemma to the inductive hypothesis.
Claim. For every word $w$ (a finite list of signed indices among the five cotree generators), the free reduction of $w$ is freely reduced.
background
Loom treats a finished recognition history as a finite list of closed walks on the eight-state, three-axis window forced by the T7 octave. Up to homotopy those walks form a free group of rank $E-V+1=5$, so each loop is a word in five signed generators (here a List Int). Spelling is not content: words are identified up to free reduction, and the module supplies a total checker that only accepts reduced words.
reduceWord is the computable free-reduction map; isReduced is the Boolean predicate that a word has no adjacent inverse pair. The sibling consRed builds a reduced word by prepending a letter and cancelling if needed; isReduced_consRed states that this constructor preserves the reduced flag when the tail is already reduced. The module carries no model or search: it only certifies finished objects.
proof idea
Term-mode proof by induction on the list structure of $w$.
- Base: $w = []$. Both sides reduce by definition;
rflcloses. - Step: $w = x :: t$. The inductive hypothesis says
reduceWord tis reduced. ApplyisReduced_consRed x (reduceWord t) ih, which is exactly the statement that prepending $x$ via the reducing constructor yields a reduced word.
No other lemmas are required; the argument is pure structural induction plus the cons-reduction invariant.
why it matters
Doc-comment frames this as the checker's specification: without it, "reduced" is aspirational. Downstream, all_isReduced_reduceConfig maps the claim over every loop of a configuration, so reduceConfig lands in the well-formed fragment. That feeds the invariant pipeline (including the depth-one abelian reading abelBag), which must only see reduced words before sorting and tracing in $\mathrm{SL}(2,\mathbb{Z}/3)$.
In the broader RS chain this sits under the Loom certificate layer for closed walks on the T7 eight-tick window ($D=3$, period 8). It does not force physics constants; it makes the free-group normal form a proved fact so conjugation-blind and spelling-blind invariants rest on theorems rather than conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.