abelian_equal_cfgCD
plain-language theorem explainer
The abelianised classical source reading assigns identical values to the second Loom discovery pair cfgC and cfgD. Anyone arguing that bag-style or abelianised sources cannot serve as the recognition-side half of the order-sensitive gravity discriminator will cite this. The proof is a one-line reduction to the already-decided equality of abelian bag maps on that pair.
Claim. Under the abelianised classical source projection (source map $S_{\mathrm{ab}}$ with equality of lists of integer lists), one has $S_{\mathrm{ab}}(\mathrm{cfgC}) = S_{\mathrm{ab}}(\mathrm{cfgD})$, where $\mathrm{cfgC}$ and $\mathrm{cfgD}$ are the second gauge-separated Loom certificate pair.
background
The module freezes the classical half of the order-sensitive gravity discovery discriminator from the G0 plan: a classical source projection is a typed reading of a Loom Config that may stand in for the conventional source. Only readings already proved equal on a gauge-separated certificate pair may inhabit the THEOREM-grade interface; identifying any such reading with continuum $T_{\mu\nu}$ remains MODEL.
AbelianProjection packages the abelianised bag map as such an interface: its source is the abelian bag reading, equality is literal list equality, and it factors through the abelianisation. The second discovery pair is cfgC ("some door is opened by every key, and every door opens every key") versus cfgD ("some door opens every key, and every key opens every door"). Upstream, abelianised_is_blind2 already records abelBag cfgC = abelBag cfgD by decision procedure.
proof idea
One-line term wrapper: the goal is definitionally the statement that the abelianised sources of cfgC and cfgD agree, which is exactly abelianised_is_blind2. No further rewriting or case analysis is required.
why it matters
Together with the depth-one equality on the same pair, this fills the "classical-equal" half of the second discovery pair in the classical source projection module. The module's honesty block states the THEOREM content is precisely these equalities and the matching depth-two separations, by reduction to Loom certificate blindness and separation lemmas. Depth-two still separates cfgC from cfgD, so the classical-equal / recognition-unequal shape is inhabited for this pair as well as for cfgA/cfgB. No continuum Einstein equation, Fin-16 seating, or claim that the depth-two residue is gravitational is asserted. Downstream use sites are not yet wired in this graph snapshot; the result stands as a certified inhabitant of the abelian classical-source interface on the second pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.