abelianSource
plain-language theorem explainer
Abelianised bag-of-relations reading of a Loom configuration: the sorted multiset of abelianised loops. Gravity analysts cite it when wiring classical source interfaces that must equalize on gauge-separated certificate pairs. The body is a one-line alias of the Loom abelian bag map.
Claim. For a Loom configuration $c$ (a finite list of closed walks sharing one basepoint), the abelian source of $c$ is the lexicographically sorted list of abelianised loop words of $c$.
background
This module freezes the classical-source half of the order-sensitive gravity discovery discriminator. A classical source projection is a typed reading of a Loom configuration that may stand in for the conventional source; only readings already proved equal on the gauge-separated certificate pair may inhabit the THEOREM-grade interface. Identifying any such reading with continuum stress-energy remains MODEL.
A Loom configuration is a finite list of closed walks (words) at a common basepoint. The upstream abelian bag map sends each word to its abelianisation and sorts the resulting multiset lexicographically, yielding a list of integer lists. That bag is order-blind: conjugacy and free reduction are quotiented out before comparison.
Sibling depth-one and depth-two readings live in the same module. Depth one and the abelian bag equalize the certificate pairs; depth two separates them.
proof idea
One-line definitional wrapper: the abelian source of $c$ is exactly the Loom abelian bag map applied to $c$ (map each word to its abelianisation, then sort lexicographically). No extra proof obligations.
why it matters
This reading is the payload of the abelian classical-source interface and the subject of decoy D2: the unique abelianised bag is blind on the discovery pair. It appears in the composite certificate that classical sources equalize while recognition (depth two) separates, inhabiting the classical-equal / recognition-unequal shape required by the frozen world G0 plan.
Downstream, the abelian projection structure packages this map with equality and a nontriviality witness; the decoy theorem is a direct reduction to the Loom abelianised-blindness lemma; the composite cfgA/cfgB theorem conjoins depth-one equality, abelian equality, and depth-two separation. Honesty boundary from the module: THEOREM for the equalities and separations; MODEL for any claim these projections are physical $T_{\mu\nu}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.