depthTwoReading
plain-language theorem explainer
Extracts the depth-two (commutator / pair-trace) half of the Loom invariant of a configuration against the certificate base table. Gravity analysts cite it as the recognition residual that separates discovery pairs while classical bag readings equalize. The body is a one-line projection of the second component of the table invariant.
Claim. For a Loom configuration $c$ (a finite list of closed walks at a common basepoint), the depth-two reading is the second component of the pair-valued invariant of $c$ evaluated on the fixed certificate homomorphism table: $\mathrm{inv}(T_{\mathrm{base}},c)_2 \in \mathrm{List}\,\mathbb{N}$. It is the commutator / pair-trace residual, not a classical source projection.
background
The module freezes the classical-source half of the order-sensitive gravity discovery discriminator from the OrderSensitive Gravity proposition. A classical source projection is any typed reading of a Loom configuration allowed to stand in for the conventional source; only readings already proved equal on gauge-separated certificate pairs may sit at theorem grade. Continuum stress-energy identification remains model-level.
A Loom configuration is an utterance: a finite list of closed walks sharing one basepoint. The core invariant of a table $T$ on a configuration returns a pair of natural-number lists (via evaluation then multiset-honest sorting). The first component supports depth-one / abelianised bag readings; the second is the depth-two residual.
The fixed table is the certificate-search homomorphism (five generator pairs). Upstream certificate lemmas already show depth-one and abelianised projections are blind on the discovery pairs, while depth-two separates them.
proof idea
Pure definitional projection: apply the Loom invariant at the certificate base table to the input configuration and return the second factor of the resulting List Nat × List Nat. No tactics, no lemmas beyond the invariant and base table constructors. Downstream separation theorems then wrap named certificate facts (depth_two_separates, depth_two_separates2) at this reading.
why it matters
This is the recognition residual the classical-source campaign asks about. It feeds the composite certificate that classical sources equalize while recognition does not: depth-one and abelian sources agree on cfgA/cfgB (and cfgC/cfgD), yet this depth-two reading differs. Sibling theorems depthTwo_separates_cfgAB and depthTwo_separates_cfgCD are one-line wrappers of the Loom separation facts at this def.
Downstream, OrderSensitiveHistoryResponse4D builds the history response and fingerprint from it (antisym edge seating of the list fingerprint), and reuses the separation as the discovery-pair certificate. In the broader RS gravity story it marks where order-sensitive structure survives after classical bag projections go blind; the module explicitly does not claim the residue is gravitational $T_{\mu\nu}$ or seats into a continuum Einstein equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.