enrichedWitness_toBare
plain-language theorem explainer
The bare J-cost shadow of the dual-entry enriched witness at real displacement d equals the sign-blind bare ledger of the ratio-substrate blocker. Gravity analysts closing Wave B residual R3 (signed-source enrichment) cite this bridge. The proof equates costs by extending through the two-hinge ratio bridge and the identity that strain is log of the witness x-ratio.
Claim. For every real displacement $d$, the bare recognition ledger of the dual-entry enriched witness at $d$ (forgetting signed debit/credit orientation) equals the sign-blind bare ledger at $d$.
background
Module setting is Wave B residual R3: dual-entry signed-source enrichment without an xRatio field on the enrichment type itself. The bare cost ledger is a derived shadow of the foundational recognition ledger, which carries two signed columns debit and credit with phi = debit - credit. The J-cost $J(x)=(x+x^{-1})/2-1$ is even and forgets exactly $\mathrm{sign}(\phi)$.
Enrichment is a dual-entry strain state: integer debit/credit columns, nonnegative magnitude, and a unit-flux cap. A global $\mathbb{Z}/2$ convention pins deficit iff debit-leads (ledger mirror of the Regge sign convention). Flipping that convention swaps columns and negates phi/strain while leaving the bare J-ledger unchanged.
Upstream, J-cost is the RS recognition cost of a positive ratio. The two-hinge witness bridge supplies a positive x-ratio whose log recovers the enriched strain; the ratio-bridge ledger cost identity converts pairwise J of ratio quotients into ledger costs.
proof idea
Apply cost-extensionality of recognition ledgers, then funext on pairs $(i,j)$. Reduce the goal to equality of $J(\exp(\Delta\mathrm{strain}))$ with the sign-blind bare cost.
Rewrite the bare side via the ratio-bridge cost lemma on the two-hinge witness bridge, so it becomes $J(x_i/x_j)$. Show strain equals $\log\circ x\mathrm{Ratio}$ by unfolding the bridge and the enriched-strain definition, then $\log\circ\exp$. Substitute both strains, apply $\exp(a-b)=\exp a/\exp b$, and cancel with $\exp\circ\log$ using positivity of the bridge ratios.
why it matters
This is the bare-shadow half of the R3 bridge: enrichment projects exactly onto the blocker's sign-blind ledger. Downstream, non-injectivity of the bare shadow on the enriched family rewrites both sides through this equality (witnesses at $+1$ and $-1$ share a bare ledger but differ in extract). The non-factorability theorem (no bare selector recovers the signed extract) and the R3 closure package both list it among the four witnesses of TypedResidual_signed_source_enrichment_schema.
In framework terms it separates the even J-cost quotient from the signed dual-entry source that gravity residuals need, without flipping gap1_bridge_derived or binding the R5 ratio-derived prop. Load-bearing content is F2 plus separation (a)(b)(c); posting-run adjacency remains garnish.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.