TypedResidual_signed_source_enrichment_schema
plain-language theorem explainer
R3 residual schema: dual-entry strain states are strictly richer than bare recognition ledgers. Extract on the two-cell witness recovers any signed source d, the bare shadow matches the sign-blind ledger, column swap leaves the bare cost unchanged, and no function of the bare ledger alone recovers extract. Gravity/QG residual auditors cite it; the body is a four-conjunct Prop packaging those separation claims.
Claim. The signed-source enrichment residual holds when: (i) for every real $d$, the dual-entry witness built from $d$ has extract at hinge $0$ equal to $d$; (ii) its bare shadow equals the sign-blind two-cell ledger of $d$; (iii) swapping debit/credit columns of any dual-entry strain state on $\mathrm{Fin}\,2$ leaves the bare ledger unchanged; (iv) no map from bare two-cell ledgers to $\mathbb{R}$ recovers extract from the bare shadow of every such witness.
background
Wave B residual R3 sits in the dual-entry signed-source enrichment module. The bare cost object RecognitionLedger on a finite lattice assigns a symmetric, diagonal-zero real cost to cell pairs. It is treated as a derived shadow of the foundational recognition ledger, whose debit and credit integer columns yield signed flux $\phi = \mathrm{debit}-\mathrm{credit}$. The J-cost quotient is even and forgets exactly $\mathrm{sign}(\phi)$.
The enrichment carrier is a dual-entry strain state: integer debit/credit columns, nonnegative magnitude, and a unit-flux cap. Global $\mathbb{Z}/2$ convention: deficit iff debit-leads (Regge-sign mirror). The witness for source $d$ places unit orientation by the sign of $d$ and magnitude $|d|$. Bare projection is the sign-blind ledger induced by the unit-coupled two-hinge bridge. Recovery means a selector on bare ledgers that reproduces extract at hinge 0 for every such witness.
proof idea
Definitional packaging only: the Prop is the conjunction of four already-named claims. No tactics. Downstream closure proves each conjunct by citing extract recovery on the witness, bare equality to the sign-blind ledger, bare invariance under column swap, and nonexistence of a bare selector (reduced to the no-selector lemma for signed sources).
why it matters
Closes residual R3 in the QG Wave B gap list: signed dual-entry state is strictly richer than the bare J-ledger shadow. Parent theorems typedResidual_signed_source_enrichment_schema_closed and its capitalized alias discharge the schema by assembling the four conjuncts. Supports the dual-entry orientation story without touching gap1 bridge derivation, recognition-ratio binding (R5), or posting-run adjacency garnish. Load-bearing content is F2 plus separations (a)(b)(c). Does not encode Freudenthal mesh geometry; carrier stays the reshaped real line from R1/R2. R0a/R0b name-binding remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.