isReduced
plain-language theorem explainer
A word in the five signed cotree generators is reduced when it has no adjacent cancelling pair. Empty and singleton words are reduced; longer words require each consecutive pair to sum nonzero and the tail to be reduced. The well-formedness checker and free-reduction lemmas cite this predicate as the decidable content of free reduction on the Loom free group.
Claim. A word $w$ (a finite list of integers, each a signed cotree generator) is reduced when it contains no adjacent cancelling pair: the empty word and every singleton are reduced, and $x::y::t$ is reduced if and only if $x+y \neq 0$ and $y::t$ is reduced.
background
In the Loom certificate language, a finished recognition history is a finite list of closed walks sharing one basepoint. On the eight-state, three-axis window fixed by the forcing chain, closed walks up to homotopy form a free group of rank $E-V+1=5$, so each loop is a word in five signed generators (here Word := List Int).
Spelling is not content: two words that free-reduce to the same reduced form represent the same loop. The predicate below is exactly the free-group reduced-word condition for that alphabet: adjacent letters that are additive inverses cancel. The module supplies a total checker for well-formed configurations and a computable conjugation-blind invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$; both rest on this Boolean test.
proof idea
Pure recursive definition on list structure. Base cases: [] and single-letter words return true. Inductive case: for head pair $x,y$ and tail $t$, return $(x+y \neq 0)$ conjoined with the recursive call on $y::t$. No lemmas; the body is the specification that later theorems (isReduced_cons_cons, isReduced_tail, isReduced_consRed, isReduced_reduceWord) unfold against.
why it matters
This is the content side of free reduction in Loom. Downstream, wellFormed requires every loop of a configuration to satisfy the predicate and to contain the frame generator. The specification theorem isReduced_reduceWord proves that the computable reducer always lands in the reduced set, so the checker's verdict is a fact rather than a wish. Closure lemmas isReduced_consRed, isReduced_tail, and all_isReduced_reduceConfig build on it so that reduction of whole utterances preserves the reduced property. In the Recognition framework this implements the module premise that spelling is not content on the free group of rank five arising from the eight-tick window (T7) and $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.