enrichedWitness
plain-language theorem explainer
Constructs a dual-entry strain state on two cells that realizes a signed source $d$: debit leads when $d\ge 0$, credit leads otherwise, with magnitude $|d|$. Gravity analysts cite it as the canonical R3 enrichment witness. The body is a pure case-split definition plus a short flux-unit proof by `simp`.
Claim. For every real $d$, there is a dual-entry strain state on $\mathrm{Fin}\,2$ whose debit column is $(1,0)$ when $0\le d$ and $(0,1)$ otherwise, whose credit column is the complementary unit vector, and whose magnitude is $|d|$ on both cells (with the unit-flux bound $|\mathrm{debit}-\mathrm{credit}|\le 1$).
background
Wave B residual R3 enriches the bare J-cost ledger by restoring dual-entry column orientation. The bare RecognitionLedger is a derived shadow of the foundational recognition ledger, which carries integer debit and credit columns with imbalance $\phi=\mathrm{debit}-\mathrm{credit}$. The J-cost quotient is even and forgets exactly $\mathrm{sign}(\phi)$.
DualEntryStrainState is the model structure: integer debit/credit maps, a nonnegative real magnitude, and a unit-flux cap $|\mathrm{debit}-\mathrm{credit}|\le 1$. Strain is the signed product $(\mathrm{debit}-\mathrm{credit})\cdot\mathrm{mag}$. The global $\mathbb{Z}/2$ pin is "deficit iff debit-leads", the ledger mirror of the Regge sign convention; flipping it swaps columns and negates strain while leaving the bare J-ledger unchanged.
The carrier here is two cells ($\mathrm{Fin},2$), not a full mesh. No field mentions $x$-ratio or real logarithms; the only real-valued field is magnitude.
proof idea
Definition by cases on the sign of $d$. When $0\le d$, cell $0$ is debited and cell $1$ credited (unit integers); when $d<0$ the columns swap. Magnitude is constantly $|d|$, with nonnegativity from abs_nonneg. The flux-unit obligation is discharged by nested by_cases on the sign of $d$ and on $\sigma=0$, each branch simplifying to $|1-0|=1$ or $|0-1|=1$.
why it matters
This is the load-bearing witness for the R3 signed-source enrichment schema in the QG Wave B residual attack. Downstream, enrichedWitness_strain computes the signed strain $(d,-d)$; enrichedWitness_extract_zero recovers the source at hinge $0$; enrichedWitness_eq_ofLedger factors the construction through ofLedger on a foundational ledger; and enrichedWitness_toBare bridges to the sign-blind bare ledger used by the blocker.
Separation theorems then fire: toBare_not_injective shows the bare shadow collapses $d$ with $-d$ while extracts differ, and RecoversExtractFromBare packages the non-existence of any bare selector that recovers the signed extract. Together these discharge the enrichment half of TypedResidual_signed_source_enrichment_schema without touching gap1-bridge derivation, ratio binding (R5), or posting-run adjacency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.