depthOne_equal_cfgCD
plain-language theorem explainer
Depth-one classical source readings of the second Loom certificate pair agree exactly. Citation target for the order-sensitive gravity discovery discriminator: bag-style additive projections cannot separate that pair. Proof is a one-line term applying the Loom lemma that depth-one invariants are blind on the pair.
Claim. Under the depth-one classical source projection (loop-by-loop bag reading of a Loom configuration, with equality as ordinary equality of the projected lists), the reading of certificate configuration $C$ equals the reading of certificate configuration $D$.
background
The module freezes the classical half of the order-sensitive gravity discovery setup from the holography plan: a classical source projection is a typed reading of a Loom Config allowed to stand in for the conventional source side of the discriminator. Only readings already proved equal on a gauge-separated certificate pair may sit at theorem grade; identifying any such reading with continuum stress-energy stays model-level.
Depth-one projection packages the depth-one source map as a SourceProjection on lists of naturals, with equality ordinary list equality and the abelian-factoring flag set. Configurations $C$ and $D$ are the second discovery pair in certificate data: $C$ encodes "some door opened by every key, and every door opens every key"; $D$ encodes the dual "some door opens every key, and every key opens every door."
Upstream, depth_one_is_blind2 states that the depth-one component of the base invariant agrees on $C$ and $D$ (proved by decide). The module doc records that additive occupation-style bag readings are blind and serve as decoy D2.
proof idea
One-line term proof: the goal is definitionally the equality of depth-one sources of $C$ and $D$ under the depth-one projection interface, which is exactly the statement of depth_one_is_blind2. No further rewriting or case analysis is required.
why it matters
Fills the second half of the classical-equal side of the discovery shape: depth-one (and abelianised) projections equalize both certificate pairs $A$/$B$ and $C$/$D$, while depth-two separates both. Together these inhabit the classical-equal / recognition-unequal pattern required by the frozen world G0 plan for order-sensitive gravity.
The result is theorem-grade only as an equality of typed Loom readings, by reduction to the Loom separation lemmas. It does not seat the residue into continuum gravity or claim a physical $T_{\mu\nu}$. Sibling theorems cover the abelianised equalities and the depth-two separations that complete the discriminator. No downstream dependents are wired yet; the declaration closes the cfgC/cfgD depth-one slot in the module's proved list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.