abelBag
plain-language theorem explainer
Depth-one reading of a Loom utterance: each closed walk is replaced by its abelianisation (five integer exponent sums), then the list is sorted lexicographically to a canonical multiset. Gravity and separation proofs cite it as the bag-of-relations projection. The body is a pure definition: map through abel, then sortLex.
Claim. For an utterance $c$ (a finite list of closed walks sharing a basepoint in the free group of rank $5$), return the lexicographically sorted list of abelianised loops, where each loop $w$ is sent to the $5$-tuple of net exponent sums of the signed generators.
background
Loom treats a finished recognition history as a configuration: a finite list of words in five signed generators (the free group of rank $E-V+1=5$ on the eight-state, three-axis window). Spelling is not content, so words are read up to free reduction; shared basepoint is not content either, so simultaneous conjugation is quotiented out.
The sibling abel computes the unique abelianisation of one word: for each generator index $i\in{0,\ldots,4}$, the count of $+ (i+1)$ minus the count of $-(i+1)$. That is the reading a bag of faces performs. abelBag lifts this to whole utterances and canonicalises the multiset by lexicographic sort.
The module invariant also records pairwise commutator traces in $SL(2,\mathbb{Z}/3)$ (depth-two lower-central data). Abelianisation destroys exactly that layer; this definition isolates the depth-one shadow used to prove blindness.
proof idea
One-line definition, not a proof. Apply abel pointwise to every word of the configuration, then sortLex on the resulting list of integer vectors so equal multisets compare equal regardless of order. No tactics, no lemmas discharged in the body.
why it matters
Supplies the classical bag-of-relations interface. Downstream, abelianSource is literally this map, feeding ClassicalSourceProjection in the gravity analysis stack. In Loom.Separation, abelianised_is_blind and abelianised_is_blind2 decide equality of abelBag on flagship pairs that the full (depth-two) invariant separates: "the unique canonical quotient a bag of relations performs, so the conflation is not an artifact of one implementation."
That contrast is the module's point: loop traces alone collide on automorphism images; commutator traces restore separation. Abelianisation is the reading that throws the commutators away. It sits on the Loom certificate path for closed recognition walks on the eight-tick window (forcing T7), not on mass or coupling numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.