SourceProjection
plain-language theorem explainer
A typed interface for classical readings of Loom configurations: a source map, an equality on sources, a flag for abelian factoring, and a nontriviality witness. Gravity analysts cite it when packaging depth-one or abelianised bag readings as the "conventional source" half of the order-sensitive discovery discriminator. It is a pure structure definition; inhabitants supply the four fields.
Claim. A classical source projection on Loom configurations is a 4-tuple $(S,\,\mathrm{src},\,{\sim},\,b)$ where $S$ is a carrier type, $\mathrm{src}$ maps each configuration to an element of $S$, ${\sim}$ is a binary relation on $S$ (the equality used by the discovery gate), $b\in\{\mathrm{true},\mathrm{false}\}$ records whether the reading ignores depth-two content, and there exist configurations $c_1,c_2$ with $\mathrm{src}(c_1)\not\sim\mathrm{src}(c_2)$. Physical stress-energy identification is not part of the data.
background
The module freezes the world G0 of the Order-Sensitive Gravity proposition: classical source projections are typed readings of a Loom configuration that may stand in for the conventional-source half of the discovery discriminator. A Loom configuration is an utterance, a finite list of closed walks (words) sharing one basepoint. Only readings already proved equal on the gauge-separated certificate pairs may inhabit the interface at theorem grade.
Upstream, multi-distinction geometry supplies binary channel configurations, and ILG carries continuum-style parameter packs; those are ambient, not fields here. The double-slit amplitude is a related bag-style sum, not used as a field. The honesty split is sharp: equalities and separations reduce to Loom certificate lemmas (depth-one and abelianised blindness, depth-two separation); any claim that a projection is continuum $T_{\mu\nu}$ remains model-level.
proof idea
No proof body: this is a structure declaration. The four fields are the entire content. Inhabitants (depth-one and abelianised projections in the same module) fill source with a concrete bag map, set Equal to propositional equality, set factorsThroughAbelian to true, and discharge nontrivial by exhibiting a certificate configuration against the empty list.
why it matters
This interface is the typed gate for the classical half of the classical-equal / recognition-unequal shape in order-sensitive gravity. Downstream, DepthOneProjection and AbelianProjection inhabit it with list-of-nats and list-of-integer-lists carriers; those feed the proved equalities on cfgA/cfgB and cfgC/cfgD and the depth-two separations that show the discriminator is inhabited. Additive occupation-style bags are thereby certified blind (decoy D2). The structure deliberately omits stress-energy identification, keeping continuum Einstein seating and Fin-16 claims out of theorem grade. It does not touch the T0–T8 forcing chain or the RCL directly; it sits in the gravity analysis layer that uses Loom separation certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.