abelian_equal_cfgAB
plain-language theorem explainer
Classical abelianised sources of the Loom discovery pair agree under ordinary equality. Gravity analysts working the G0 frozen world of order-sensitive gravity cite this to show abelian readings cannot discriminate the pair. The proof is a one-line reduction to the loom lemma that abelianisation is blind on certificate data.
Claim. Under the abelianised classical source projection, the projected sources of the discovery configurations $A$ and $B$ are equal (as lists of integer lists).
background
The module freezes world G0 from the order-sensitive gravity plan: a classical source projection is a typed reading of a Loom Config allowed to stand in for the conventional-source half of the discovery discriminator. Only readings already proved equal on the gauge-separated certificate pair may sit at theorem grade; identifying any such reading with continuum stress-energy remains model-level.
The abelianised projection packages an abelian source map with ordinary equality, flags that it factors through abelianisation, and is nontrivial on the discovery pair. Configurations $A$ and $B$ are the fixed Loom certificate pair (door/key style integer-list data). Upstream, abelianised_is_blind is the loom separation fact that abelianised readings cannot tell those certificates apart.
Sibling depth-one (additive/occupation bag) readings are likewise blind; depth-two is the first reading that separates.
proof idea
One-line term wrapper: the claim is exactly the instance of the loom lemma that abelianised readings are blind on the certificate pair, specialized to the abelian classical-source interface (source map plus equality). No extra algebra or case split.
why it matters
Fills the G0 abelian slot on the discovery pair: classical abelianised sources of $A$ and $B$ agree. Together with the matching depth-one equality and the depth-two separation on the same pair, it inhabits the classical-equal / recognition-unequal shape required by the order-sensitive gravity proposition. The module honesty clause is explicit: theorem grade covers only these equalities and separations by reduction to loom blindness and separation lemmas; any claim that the projection is physical $T_{\mu\nu}$, a continuum Einstein equation, a Fin-16 seating, or that the depth-two residue is gravitational is out of scope. No downstream consumers are wired yet; the result is infrastructure for the G0 discriminator interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.