enrichedWitness_extract_zero
plain-language theorem explainer
For any real signed source d, the dual-entry enrichment witness recovers d exactly when its extract is evaluated on the first of two cells. Gravity and QG residual work cites this as the load-bearing recovery identity for signed-source enrichment (R3). The proof is a one-line simplification through the extract definition and the strain formula of the witness.
Claim. For every real number $d$, if $W(d)$ is the dual-entry strain state on two cells that realizes signed source $d$ (debit-leads when $d \ge 0$, magnitude $|d|$), then the extract of $W(d)$ at cell $0$ equals $d$.
background
Wave B residual R3 treats the bare cost ledger as a shadow of the foundational recognition ledger, which carries two signed integer columns debit and credit with $\phi = \mathrm{debit} - \mathrm{credit}$. The J-cost quotient is even and forgets $\mathrm{sign}(\phi)$. Enrichment restores orientation via a dual-entry strain state: integer debit/credit columns, nonnegative magnitude, and a unit-flux cap.
The global $\mathbb{Z}/2$ convention is deficit iff debit-leads (the ledger mirror of the Regge sign convention). Flipping it swaps columns and negates $\phi$/strain while leaving the bare J-ledger unchanged.
The dual-entry witness for a real $d$ places a unit debit/credit pair on $\mathrm{Fin},2$ according to the sign of $d$, with magnitude $|d|$ on both cells. Its strain theorem states that strain equals $d$ on cell $0$ and $-d$ on cell $1$. Extract is the strain readout used as the signed source.
proof idea
Term-mode one-liner. Unfold extract on the dual-entry strain state and rewrite by the strain identity for the enriched witness: strain at cell $0$ is exactly $d$. The simp call discharges the equality with no case split at this layer (cases live inside the strain lemma).
why it matters
This is the recovery half of R3 separation. The closed residual packages it with the bare-shadow map, the swap identity, and the non-factorability theorem: no bare-ledger selector recovers the enriched extract. Downstream, non-injectivity of the bare shadow on the witness family uses the extract identity at $\pm 1$ to show opposite sources share a bare image yet differ after extract. The schema-closure theorem lists this lemma first in its witness tuple, so R3 is discharged only with this recovery in hand.
In the broader Recognition gravity stack the point is structural: signed source is not a bare J-ledger observable; dual-entry orientation is required. The module deliberately leaves R0a/R0b name-binding and posting-run adjacency open; this lemma does not touch those gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.