enrichedWitnessLedger
plain-language theorem explainer
A two-unit foundational ledger encoding the dual-entry orientation of a signed real source d. Debit and credit columns on the two-point carrier flip with sign(d), so phi = debit - credit carries unit flux of the matching orientation. Gravity analysts closing the R3 signed-source enrichment cite it as the concrete Recognition ledger behind the enriched witness. The body is a pure definition by cases on the sign of d.
Claim. For each real $d$, define a recognition ledger on the two-point discrete carrier $\{0,1\}$ by $\mathrm{debit}(\sigma)=\mathbf{1}_{\sigma=0}$ and $\mathrm{credit}(\sigma)=\mathbf{1}_{\sigma=1}$ when $d\ge 0$, and the swapped assignment when $d<0$. Then $\phi=\mathrm{debit}-\mathrm{credit}$ has absolute value one at each unit, with overall orientation matching $\mathrm{sign}(d)$ under the global $\mathbb{Z}/2$ deficit-iff-debit-leads convention.
background
The module attacks Wave B residual R3: dual-entry signed-source enrichment without xRatio. The bare cost ledger is treated as a derived shadow of the foundational recognition ledger, which carries two signed integer columns debit and credit on the units of a recognition structure, with $\phi=\mathrm{debit}-\mathrm{credit}$. The J-cost quotient is even and forgets exactly $\mathrm{sign}(\phi)$; the enrichment restores that orientation as dual-entry column data with nonnegative magnitude and a unit-flux cap.
A discrete carrier on a finite type $\Lambda$ is the recognition structure whose units are $\Lambda$ and whose relation is total (carrier-only; no posting graph). Here $\Lambda=\mathrm{Fin},2$, so there are exactly two units. The foundational ledger structure is simply a pair of maps $\mathrm{debit},\mathrm{credit}:U\to\mathbb{Z}$.
The global $\mathbb{Z}/2$ pin is: deficit iff debit-leads, the ledger mirror of the Regge sign convention. Flipping the convention swaps columns and negates $\phi$ and strain while leaving the bare J-ledger unchanged.
proof idea
Pure definitional construction, not a proof. On the two-point carrier, debit and credit are defined by nested case splits on $0\le d$ and on whether the unit is $0$. Nonnegative $d$ puts unit debit on $0$ and unit credit on $1$; negative $d$ swaps the columns. No lemmas are invoked; the fields are closed integer-valued functions of the unit.
why it matters
This is the type-level anchor that makes the enriched witness a genuine restriction of a foundational ledger rather than a free-standing record. Downstream, the equality theorem states that the enriched witness equals the ofLedger projection of this ledger at magnitude $|d|$, discharged by rfl once the unit-flux bound is in hand. The companion bound proves $|\phi|\le 1$ at every unit by the same case split, discharging the flux-unit hypothesis of ofLedger.
In the R3 program this closes the honesty claim that DualEntryStrainState.ofLedger builds the enrichment from an actual Recognition.Ledger on discreteCarrier, with the equality and flux theorems as Lean facts rather than docstring citations. It does not touch gap1_bridge_derived, does not bind recognition_ratio_derived (R5), and leaves R0a/R0b name-binding and posting-run adjacency as open garnish. Load-bearing content remains F2 plus the separation clauses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.