abel
plain-language theorem explainer
Abelianisation of a closed recognition walk: the net exponent vector in ℤ⁵ of the five signed cotree generators. Anyone reading Loom configurations, bag-of-faces content, or circle-winding residuals cites this as the unique canonical quotient of a word. The body is pure counting: for each generator index it subtracts the length of the negative occurrences from the positive ones, with no free reduction.
Claim. Let $w$ be a word in the five signed cotree generators (a finite list of integers from $\{\pm 1,\ldots,\pm 5\}$). Its abelianisation is the length-5 integer vector whose $i$-th entry ($i=0,\ldots,4$) equals $\#\{x\in w:x=i+1\}-\#\{x\in w:x=-(i+1)\}$. Equivalently, this is the image of $w$ under the canonical map from the free group of rank $5$ to $\mathbb{Z}^5$.
background
Loom treats finished recognition histories as closed walks on the eight-state, three-axis window forced by the T0–T8 chain. Homotopy classes of such walks form a free group of rank $E-V+1=5$, so a closed walk is a word in five signed generators and an utterance is a finite list of such words sharing a basepoint.
A Word is exactly that list of integers: each entry is a signed generator label. Content is read up to free reduction (spelling is not content) and, under the basepoint/vertex-homogeneity stance of the module, up to simultaneous conjugation. The module supplies a total well-formedness checker, a computable invariant (traces in $\mathrm{SL}(2,\mathbb{Z}/3)$ plus pairwise commutator traces), and theorems that the invariant is blind to those two non-content operations.
Abelianisation is the coarser reading that keeps only net exponent sums. The module doc notes that loop traces alone fail to separate the intended witness and that commutator (depth-two) data is exactly what an abelianised reading destroys; this definition is that abelianised reading.
proof idea
Definition by direct construction, not a proved theorem. Range over the five generator indices $i\in{0,1,2,3,4}$. For each $i$, filter the input list for entries equal to $+(i+1)$ and for entries equal to $-(i+1)$, take ordinary list lengths, and subtract. The result is a List Int of length 5. No free reduction, sorting, or conjugation is applied; raw occurrence counts determine the exponent vector.
why it matters
This is the bag-of-faces quotient named in the doc-comment: the unique canonical abelian image of a closed walk. Downstream, circle-winding material uses exponent-sum data when extracting directed cycles, comparing residuals to the fundamental cycle, and showing that closed-generator lists are generated by that cycle modulo a boundary (directedCycleExtraction, closedSingularOneCycleList_boundary_generate_of_residual_bound, and related free-boundary lemmas). In the Loom stack it is the reading against which the deeper $\mathrm{SL}(2,\mathbb{Z}/3)$ invariant is contrasted: abelianisation erases the commutator traces the invariant needs.
Framework landmark: free rank 5 on the eight-tick, three-axis window (T7 octave, T8 $D=3$). The definition does not itself force physics constants; it is infrastructure for certificates of closed recognition walks and for homological bookkeeping of windings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.