classicalEqual_recognitionUnequal_cfgAB
plain-language theorem explainer
On the gauge-separated Loom pair cfgA/cfgB, the depth-one and abelianised classical source projections agree while the depth-two (commutator) reading differs. Anyone citing the classical-equal / recognition-unequal discriminator for order-sensitive gravity needs this composite. The proof is a one-line term packing the three Separation lemmas already proved by decide.
Claim. For the certificate configurations $A$ and $B$, the depth-one (loop-by-loop amplitude bag) sources coincide, the abelianised bag-of-relations sources coincide, and the depth-two (commutator / pair-trace) readings are unequal.
background
The module freezes 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 a gauge-separated certificate pair may inhabit the THEOREM-grade interface. Identifying any such reading with continuum stress-energy remains MODEL.
Depth-one source extracts the first component of the base invariant (loop-by-loop / amplitude bag). Abelianised source is the canonical quotient of the bag of relations. Depth-two reading is the second component (commutator / pair-trace); it is explicitly not a classical source, but the recognition residual the campaign asks about.
Upstream, depth_one_is_blind and abelianised_is_blind prove the two classical projections equalize cfgA and cfgB (the latter "the unique canonical quotient a bag of relations performs"), while depth_two_separates proves the residual differs on exactly one coordinate of a finite set.
proof idea
Term-mode one-liner: the conjunction is the triple of upstream Separation theorems
depth_one_is_blind, abelianised_is_blind, and depth_two_separates,
re-exported under the local classical-source names. No new computation; the equalities and the inequality are already discharged by decide on the finite certificate data.
why it matters
This is the composite certificate that the classical-equal / recognition-unequal shape is inhabited on cfgA/cfgB. The module doc states the campaign goal explicitly: depth-one and abelianised projections equalize the pair, depth-two separates, so the discriminator is realized at THEOREM grade. Additive / occupation-style bag readings are thereby flagged as blind (decoy D2).
No downstream Lean consumers yet (used_by empty); the declaration closes the G0 half of the frozen plan rather than feeding a larger proof chain. It does not touch the T0–T8 forcing landmarks, RCL, or the alpha band; its role is local to order-sensitive gravity and the Loom separation certificates. Continuum identification with $T_{\mu\nu}$ and any claim that the depth-two residue is gravitational remain open MODEL questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.