isReduced_cons_cons
plain-language theorem explainer
For a word with at least two letters, freeness under cancellation factors as: the head pair does not sum to zero, and the suffix from the second letter is already reduced. Anyone proving facts about free reduction on Loom words cites this. The proof is definitional reflexivity against the recursive clause of the reducedness predicate.
Claim. For integers $x,y$ and a word $t$ (a list of signed generator indices), a word $x::y::t$ is freely reduced if and only if $x+y \neq 0$ and $y::t$ is freely reduced.
background
Loom treats closed recognition walks on the eight-state, three-axis window as words in five signed cotree generators. A Word is simply a list of integers. Content is read up to free reduction: adjacent inverse pairs cancel and are not part of the meaning.
The predicate isReduced is the total Boolean checker for that freeness. Empty and singleton words are reduced; a longer word $x::y::t$ is reduced exactly when the head pair does not cancel ($x+y \neq 0$) and the suffix $y::t$ is reduced. That recursive clause is the mathematical content of this declaration.
The module supplies a well-formedness checker, a computable conjugacy-blind invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and theorems that the invariant ignores free reduction and simultaneous conjugation. This lemma is pure list algebra supporting the reduction side.
proof idea
One-line definitional proof: rfl. The right-hand side is literally the third equation clause of isReduced, so the equality holds by unfolding.
why it matters
Free reduction is one of the two non-content operations the Loom invariant must ignore. This unfolding lemma is the workhorse for inductive arguments on reduced words.
It is used by isReduced_tail, which extracts reducedness of a proper suffix from reducedness of a cons cell, and by isReduced_consRed, which shows that the smart constructor consRed always returns a reduced word. Those facts underwrite the total reducer and the claim that the checker is sound on finished certificates.
In the broader Recognition picture this sits under the eight-tick, rank-five free group of closed walks (forcing chain T7 and the $E-V+1=5$ count). It does not touch J-cost, phi, or the mass ladder; it is infrastructure for the certificate language that records closed histories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.