perm_append_left_comm
plain-language theorem explainer
Concatenating three finite lists as A then B then P yields a permutation of B then A then P. Loom cites this when showing that reordering the loops in an utterance does not change the multiset of pairwise commutator traces. The proof reassociates both sides and applies right-append to the two-list commute.
Claim. For any finite lists $A$, $B$, and $P$ of natural numbers, the concatenations $A{+}{+}(B{+}{+}P)$ and $B{+}{+}(A{+}{+}P)$ are permutations of each other (same elements with the same multiplicities, possibly different order).
background
The Loom module treats a finished recognition utterance as a finite list of reduced words in the free group of closed walks on the eight-state, three-axis window (rank $E-V+1=5$). Content is defined negatively: free reduction is not content, and simultaneous conjugation of every loop is not content. The module supplies a total well-formedness checker and a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, including traces of pairwise commutators (depth-two lower-central data), which is blind exactly to those two non-content operations.
This lemma is pure list combinatorics on List Nat. It does not mention matrices or free groups. It is the elementary reordering fact needed when an utterance is permuted as a list: the tail after two prefixes can be held fixed while the prefixes swap. Mathlib supplies list permutation and append association; the local proof only packages the left-commute form used downstream.
proof idea
Short tactic proof. Rewrite both sides with reverse append-associativity so the goals become $(A{+}{+}B){+}{+}P$ and $(B{+}{+}A){+}{+}P$. Then apply List.Perm.append_right at the common suffix $P$ to the standard fact List.perm_append_comm (that $A{+}{+}B$ is a permutation of $B{+}{+}A$). No induction and no Loom-specific structure.
why it matters
Parent use is pairTraces_perm in the same module: the pairwise commutator traces of a reordered utterance form the same multiset, and the swap case is where commutator-trace symmetry is spent. That theorem is part of the certificate that the Loom invariant is blind to reordering of loops in a finished utterance, matching the module claim that spelling order of simultaneous loops is not content.
In the broader Recognition picture this sits under the Loom certificate layer for closed walks forced by the eight-tick octave and $D=3$ window (forcing chain T7–T8), not under mass ladders or $\alpha$. It is infrastructure: without left-commute of append under permutation, the induction on list permutations for pair-traces cannot discharge the swap constructor cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.