DepthOneProjection
plain-language theorem explainer
The depth-one classical source projection packages the loop-by-loop amplitude-bag reading of a Loom configuration as a typed classical-source interface. Workers on the order-sensitive gravity discriminator (G0) cite it when showing conventional bag readings equalize gauge-separated certificate pairs. It fills the interface fields with the depth-one extractor, propositional equality, an abelian-factor flag, and a nontriviality witness (cfgA versus the empty configuration).
Claim. The depth-one projection is the classical source interface on Loom configurations whose source map sends each configuration $c$ to its depth-one amplitude bag (a list of natural numbers), whose equality relation is propositional equality of bags, which factors through abelianisation, and which is nontrivial: there exist configurations with unequal bags.
background
In the 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 gauge-separated certificate pairs may inhabit the interface at theorem grade; identifying any such reading with continuum stress-energy remains model-level.
The depth-one source extracts the first component of the base invariant of a configuration: a list of natural numbers recording the loop-by-loop amplitude bag. The ambient structure packages four fields: the source map, an equality relation for the discovery gate, a boolean recording whether the reading ignores depth-two content, and a nontriviality witness that the source is not constant.
Depth-two readings (commutator / pair-trace) are deliberately excluded from this interface; they are the recognition residual the campaign asks about, not a classical source.
proof idea
Structure instance, not a theorem proof. The source field is the depth-one extractor (first component of the base invariant). Equality is propositional equality on lists of naturals. The abelian-factor flag is set true, recording that the bag reading ignores depth-two content. Nontriviality is discharged by exhibiting certificate configuration A and the empty configuration, then deciding that their depth-one bags differ.
why it matters
This definition is the carrier for the G0 depth-one equalities. The sibling theorems that classical depth-one sources of cfgA/cfgB (and cfgC/cfgD) agree both apply this projection's equality to the pair sources, reducing to the Loom blindness lemmas. Together with the abelianised projection and the depth-two separations, it inhabits the classical-equal / recognition-unequal shape of the discovery discriminator: additive occupation-style bag readings are blind (decoy D2).
Physical identification with continuum $T_{\mu\nu}$ is explicitly not claimed; the module marks that as MODEL. No continuum Einstein equation, Fin-16 seating, or gravitational reading of the depth-two residue is asserted here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.