depthOne_equal_cfgAB
plain-language theorem explainer
Classical depth-one sources of the gauge-separated Loom certificate pair A and B agree as lists of naturals. Gravity analysts working the G0 order-sensitive discriminator cite this to lock the classical-equal half of the discovery shape. The proof is a one-line wrapper of the Loom depth-one blindness lemma.
Claim. Under the depth-one classical source projection (the loop-by-loop multiset reading of a Loom configuration), the sources of certificate configurations $A$ and $B$ are equal: $\mathrm{src}_1(A)=\mathrm{src}_1(B)$ as lists of naturals.
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 a gauge-separated certificate pair may inhabit the interface at theorem grade. Identifying any such reading with continuum stress-energy remains model-level.
Depth-one projection packages the loop-by-loop (additive / occupation-style bag) reading as a SourceProjection on List Nat, with equality ordinary list equality and the flag that it factors through the abelianised quotient. Configurations $A$ and $B$ are the standard Loom certificate pair (door/key duals) that recognition depth two separates.
Upstream, depth_one_is_blind states that the loop-by-loop reading is blind on that pair: identical on $A$ and $B$. Any carrier whose reading of an utterance is a multiset of per-loop quantities therefore conflates $A$ with $B$.
proof idea
One-line term wrapper: the goal is definitionally the equality of depth-one sources of $A$ and $B$, which is exactly the statement of the Loom lemma that the depth-one (loop-by-loop) invariant is blind on the certificate pair. No extra rewriting or case analysis.
why it matters
Fills the G0 depth-one clause of the classical source projection ledger: depth-one and abelianised projections equalize $A$/$B$ (and $C$/$D$), while depth two separates both pairs, so the classical-equal / recognition-unequal shape is inhabited. The module marks additive bag readings as decoy D2: blind classical sources cannot carry the order-sensitive residue.
No downstream dependents are wired yet; the sibling suite (abelian_equal_cfgAB, depthTwo_separates_cfgAB, and the $C$/$D$ copies) jointly close the theorem-grade half of G0. Framework role is local to the gravity discriminator, not a forcing-chain (T0–T8) step. Continuum Einstein seating and any claim that the depth-two residue is gravitational remain explicitly unclaimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.