DualEntryStrainState
plain-language theorem explainer
A dual-entry strain state on a carrier Λ packages integer debit and credit columns, a nonnegative magnitude, and a unit-flux bound |debit−credit|≤1. Strain is the signed product (debit−credit)·mag; the bare J-cost ledger is the even shadow that forgets sign. Gravity and QG residual work cite it as the R3 enrichment of RecognitionLedger. The declaration is a structure definition with derived maps (phi, strain, extract, toBare, swap).
Claim. A dual-entry strain state on a carrier $\Lambda$ consists of maps $\mathrm{debit},\mathrm{credit}:\Lambda\to\mathbb{Z}$ and $\mathrm{mag}:\Lambda\to\mathbb{R}$ such that $\mathrm{mag}\ge 0$ pointwise and $|\mathrm{debit}(i)-\mathrm{credit}(i)|\le 1$ for every $i\in\Lambda$. Column imbalance is $\phi(i)=\mathrm{debit}(i)-\mathrm{credit}(i)$; signed strain is $\phi(i)\cdot\mathrm{mag}(i)$.
background
Wave B residual R3 enriches the bare cost ledger so that signed source data survive the J-even quotient. The foundational recognition ledger carries two integer columns debit and credit with imbalance $\phi=\mathrm{debit}-\mathrm{credit}$. The recognition cost $J(x)=(x+x^{-1})/2-1$ is even in the underlying ratio sense and therefore forgets exactly $\mathrm{sign}(\phi)$.
DualEntryStrainState is the model of that enrichment on an arbitrary carrier $\Lambda$: integer debit/credit, nonnegative magnitude, and a unit-flux cap so orientation is at most one quantum. The module convention pins one global $\mathbb{Z}/2$ choice (deficit iff debit-leads), mirroring the Regge sign convention used for mesh geometric deficit. Swapping columns negates $\phi$ and strain while leaving the bare J-ledger unchanged.
Upstream cost infrastructure supplies $J$ and total recognition cost under ratio weights; RS-native units fix $c=1$ gauge. No field of the structure mentions ratio logarithms or $x$-ratio data; those remain outside R3 scope.
proof idea
Definitional structure, not a proved theorem. Fields are declared directly: debit and credit as $\Lambda\to\mathbb{Z}$, mag as $\Lambda\to\mathbb{R}$ with pointwise nonnegativity, and flux_unit as the bound $|\mathrm{debit}-\mathrm{credit}|\le 1$.
Derived maps are one-line: phi is debit minus credit; strain multiplies the integer imbalance by mag; extract aliases strain; toBare (on finite decidable carriers) feeds strain into the coboundary strain ledger constructor; swap exchanges debit and credit, reuses mag_nonneg, and discharges flux_unit by absolute-value commutativity of subtraction.
why it matters
R3 is the dual-entry signed-source enrichment residual in the QG Wave B gap plan: the bare RecognitionLedger is only a J-even shadow of the foundational two-column ledger. This structure is the type-level model that restores column orientation without smuggling ratio or log fields.
It anchors later witnesses (enriched witness, ofLedger construction from a discrete carrier, swap-evenness of the bare factor) that separate signed strain from the forgetful J-cost ledger. Framework-wise it sits in the gravity analysis stack that bridges recognition ledgers to geometric deficit conventions, not in the T0–T8 forcing chain itself.
Module honesty: it does not flip the gap-1 bridge derivation, does not bind the recognition-ratio derived proposition (R5), and leaves R0a/R0b name-binding and posting-run adjacency as open garnish. Load-bearing content is F2 plus the signed/bare separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.