enrichedWitness_strain
plain-language theorem explainer
The dual-entry enrichment witness for a signed real source d carries strain d on cell 0 and -d on the other cell of Fin 2. Gravity analysts closing the R3 signed-source residual cite this when recovering the source or projecting to the bare J-ledger. The argument is definitional: funext plus case splits on the sign of d and the cell index, reducing through strain, phi, and the witness columns.
Claim. For every real $d$, the strain of the dual-entry enrichment witness realizing signed source $d$ on two cells equals the map sending cell $0$ to $d$ and every other cell to $-d$.
background
Wave B residual R3 enriches the bare cost ledger by restoring the dual-entry orientation that the even J-cost forgets. The foundational recognition ledger carries integer debit and credit columns with $\phi=\mathrm{debit}-\mathrm{credit}$; the bare J-ledger is the sign-blind shadow. DualEntryStrainState packages those columns on a discrete carrier, a nonnegative magnitude, and a unit-flux orientation cap, under the global $\mathbb{Z}/2$ convention that deficit means debit-leads (the ledger mirror of the Regge sign convention).
The witness enrichedWitness d is the two-cell realization on $\mathrm{Fin},2$: magnitude $|d|$ everywhere, and debit/credit swapped according as $0\le d$ or not, so that debit leads precisely when $d$ is nonnegative. Strain is the per-cell charge read off that dual-entry state (via $\phi$ and magnitude). This lemma records the explicit strain field of that witness.
proof idea
Term-style tactic proof. Apply functional extensionality on the cell $\sigma$. Unfold the dual-entry strain (and its $\phi$ intermediate) together with the witness definition. Case on $0\le d$: the witness columns freeze, and the absolute value simplifies by abs_of_nonneg or abs_of_neg. Inside each branch, case on $\sigma=0$ versus not; both subcases reduce by simp to the claimed piecewise values $d$ and $-d$.
why it matters
Load-bearing identity for the R3 dual-entry enrichment in the QG Wave B attack on the signed-source residual. Downstream, enrichedWitness_extract_zero recovers the source by reading extract at cell 0 through this strain formula, and enrichedWitness_toBare bridges the enrichment to the blocker's sign-blind bare ledger via cost extensionality. Together they show the enrichment is faithful on the signed source while its bare shadow matches the existing J-ledger, without touching gap1_bridge_derived, xRatio, or posting-run adjacency. Anchors the honesty claim that ofLedger builds enrichment from a real foundational ledger rather than a docstring citation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.