AbelianProjection
plain-language theorem explainer
Packages the abelianised bag-of-relations reading of Loom configurations as a classical source interface on list-of-integer-lists. Anyone citing the G0 abelian equalities on the discovery pairs (cfgA/cfgB, cfgC/cfgD) uses this instance. The construction wires the abelian source map, propositional equality, an abelian-factor flag, and a decide-checked nontriviality witness.
Claim. The abelianised classical source projection is the interface whose source map sends each Loom configuration to its abelianised bag of relations (a list of lists of integers), whose equality is ordinary propositional equality on that carrier, which factors through abelianisation, and which is nontrivial: there exist configurations with unequal abelianised sources.
background
Module setting is frozen world G0 of the order-sensitive gravity proposition: 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 inhabit the interface at theorem grade; identifying any such reading with continuum stress-energy remains model-level.
SourceProjection is the typed interface: a source extractor Config → Source, an equality relation used by the discovery gate, a Boolean recording whether the reading ignores depth-two content, and a nontriviality witness that some pair of configs has unequal sources. Physical $T_{\mu\nu}$ identification is deliberately not a field.
The source map here is the abelianised bag-of-relations projection (abelSource), which collapses each configuration to a list of integer lists and is known upstream to be blind on the certificate pairs.
proof idea
Structure-instance definition, not a deep proof. Fill four fields: source is the abelianised bag map; Equal is propositional equality on List (List Int); factorsThroughAbelian is the constant true; nontriviality is exhibited by the pair (cfgA, []) with the inequality discharged by decide.
why it matters
Inhabits the classical-source half of the G0 discovery discriminator for order-sensitive gravity. Downstream theorems abelian_equal_cfgAB and abelian_equal_cfgCD cite this instance to state that abelianised sources of cfgA/cfgB (and cfgC/cfgD) agree, each reducing to the corresponding abelianised_is_blind lemma.
Together with the depth-one projection (also blind) and the depth-two reading (which separates both pairs), this closes the classical-equal / recognition-unequal shape at theorem grade. It does not seat the residue into continuum gravity; the module honesty clause keeps continuum Einstein and $T_{\mu\nu}$ identification at MODEL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.