depthOneSource
plain-language theorem explainer
Depth-one classical source of a Loom configuration: the loop-by-loop amplitude bag, returned as a list of natural numbers. Anyone building classical-equal / recognition-unequal certificates or decoy-blindness statements cites this reading. The body is a one-line projection of the base invariant onto its first component.
Claim. For a Loom configuration $c$, the depth-one source is the first component of the base invariant of $c$, a list of natural numbers recording the loop-by-loop (amplitude-bag) reading.
background
The module freezes world G0 from the order-sensitive gravity campaign. 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 the gauge-separated certificate pair may inhabit the THEOREM-grade interface; identifying any such reading with continuum stress-energy remains MODEL.
Depth one means the additive, occupation-style bag of loop amplitudes. It is deliberately coarser than the depth-two (commutator / pair-trace) residual that the campaign uses as the recognition side. The sibling abelianised bag is the unique commutative collapse of the same data. Upstream, the base invariant of a configuration packages these graded readings; this definition simply selects the depth-one slot.
The local honesty contract is explicit: equalities and separations reduce to Loom certificate lemmas (depth_one_is_blind, abelianised_is_blind, depth_two_separates and cfgC/cfgD siblings). Continuum Einstein equations, Fin-16 seating, and gravitational status of the depth-two residue are not claimed.
proof idea
Pure definition, not a proof. The body projects (invariant base c) onto its first component, yielding List Nat. No tactics, no lemmas applied at this site; downstream theorems supply the equalities by invoking depth_one_is_blind on this reading.
why it matters
This is the concrete classical half of the discovery discriminator. It is wired into DepthOneProjection (the SourceProjection interface instance with equality and the abelian-factor flag), into decoy D2 (decoy_depthOne_blind_on_discovery and the 4D history twin), and into the composite certificates classicalEqual_recognitionUnequal_cfgAB, finiteCertificate_cfgAB, and orderSensitive_finite_gate_cfgAB.
Those parents establish the classical-equal / recognition-unequal shape: depth-one (and abelian) bags agree on cfgA/cfgB while depth-two and history response separate them, and the response difference lies outside the metric-edge image. In the order-sensitive gravity proposition this supplies the THEOREM-grade witness that additive bag readings are blind, so any continuum identification of this projection with $T_{\mu\nu}$ would miss the recognition residual the campaign isolates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.