isReduced_tail
plain-language theorem explainer
If a word with a leading signed generator is free-reduced, its tail is free-reduced. Certificate and free-group work on Loom configurations cites this when peeling heads under the reducedness checker. The proof is a two-case split on the tail that unfolds the recursive Boolean definition and projects the second conjunct.
Claim. Let $y \in \mathbb{Z}$ and let $r$ be a word in the five signed generators. If the concatenated word $y :: r$ is free-reduced (no adjacent pair sums to zero), then $r$ itself is free-reduced.
background
Loom treats a finished recognition history as a finite list of closed walks sharing one basepoint. On the eight-state, three-axis window the forcing chain supplies, closed walks up to homotopy form a free group of rank five, so each loop is a word in five signed generators. Content ignores spelling, so words are read up to free reduction: no adjacent cancelling pair.
A word is a list of integers. The reducedness predicate returns true on the empty and singleton lists, and on $x :: y :: t$ it requires $x + y \neq 0$ together with reducedness of the tail $y :: t$. The companion unfolding lemma states that equality exactly: reducedness of a two-or-more-element list is the Boolean conjunction of the non-cancellation test and reducedness of the suffix.
This lemma is the tail-stability half of that recursive checker. It lives in the certificate layer that supplies a total well-formedness test and an SL(2, Z/3Z) trace invariant blind to free reduction and simultaneous conjugation, with no model or search attached.
proof idea
Case-split on the tail $r$. If $r$ is empty, reducedness of the empty word is definitionally true, so rfl closes. If $r = z :: t$, rewrite the hypothesis with the unfolding lemma for reducedness of a cons-cons list: the hypothesis becomes the Boolean conjunction $(y + z \neq 0) \land \mathrm{isReduced}(z :: t)$. Project the second factor via the standard Boolean-and-equals-true elimination, which is exactly reducedness of $r$.
why it matters
Free reduction is one of the two non-content operations the Loom invariant must ignore. Tail stability lets later lemmas rebuild reducedness after a head is prepended or cancelled. The sole recorded consumer is the theorem that prepending a generator via the reducing cons operation preserves reducedness: that proof cases on the target word and, when a cancellation occurs, needs the tail of an already-reduced word to stay reduced.
In the broader Recognition setting this sits under the eight-tick octave and $D = 3$ window (forcing chain T7–T8): closed walks on that window are the free group of rank five, and the certificate language only trusts finished objects after free reduction. The lemma is pure list algebra; it does not touch the SL(2, Z/3Z) trace or commutator layer, but it is load-bearing for the well-formedness side of the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.