ratioBridgeLedger_cost
plain-language theorem explainer
The recognition ledger induced by a ratio bridge has pairwise cost equal to the J-cost of the comparison-ratio quotient between the two hinges. Seven Gaps and gravity-bridge authors cite this when separating ledger observables from signed geometric deficits. The proof is a short term rewrite: coboundary strain is written as exp of a log difference, which cancels to the plain ratio by positivity of xRatio.
Claim. For any finite hinge type $H$ and any recognition-ratio bridge $B$ on $H$, the cost of the induced recognition ledger between hinges $\sigma$ and $\tau$ equals $J(x_\sigma/x_\tau)$, where $x$ is the positive comparison-ratio field of $B$ and $J(t)=(t+t^{-1})/2-1$.
background
This module is Seven Gaps Phase 0a: the paper's odd recognition-ratio bridge (Def 6.2), not the refuted ledger-equals-signed-hinge form. A RecognitionRatioBridge on hinge type $H$ supplies a positive comparison ratio $x_\sigma$, a coupling $\kappa_\sigma$, a signed geometric deficit $\delta_\sigma$, a mesh scale, and a remainder bound, linked by the odd admissibility relation $\log x_\sigma=\kappa_\sigma\delta_\sigma+$remainder with cubic mesh control.
The RS cost is $J(t)=(t+t^{-1})/2-1$ (equivalently $\cosh(\log t)-1$), the unique cost forced by the Recognition Composition Law (T5). The induced object ratioBridgeLedger builds a genuine RecognitionLedger whose pairwise cost is the J-cost of the ratio quotient, realized through the proved coboundary-strain ledger on $\log\circ x$.
Upstream no-gos already force ledger deficits nonnegative and even under ratio parity, while signed Regge response is odd. The bridge keeps signed information in $\log x$; the ledger sees only even J-data. This theorem names that cost identification explicitly.
proof idea
Term-mode proof, not a wrapper of a named lemma. The ledger cost is definitionally the J-cost of the coboundary strain $\exp(\log x_\sigma-\log x_\tau)$. The goal is rewritten to that form, then Real.exp_sub and two applications of Real.exp_log (using xRatio_pos at $\sigma$ and $\tau$) cancel the exp/log pair and yield $J(x_\sigma/x_\tau)$.
why it matters
This is the cost clause that makes every ratio bridge induce a real RecognitionLedger, so the sign and parity no-gos apply to the ledger side while the odd bridge retains signed geometry in $\log x$. Downstream, twoHingeWitness_ledger_deficit_even uses it (via the induced ledger) to show the witness family's ledger deficit is even under $d\mapsto -d$, quoting the no-go family theorem on ratio-parity. signBlindBareLedger_neg_eq rewrites bare-ledger costs through the same J-of-ratio identity to prove orientation reversal leaves the bare ledger unchanged. enrichedWitness_toBare extends that identification into the 4D dual-entry enrichment analysis.
In the framework, this sits under the J-uniqueness landmark (T5) and the Seven Gaps program reconciling substrate ledgers with geometric hinge data. The bridge structure itself remains MODEL tier (admissibility hypothesis, paper Def 6.2); the named cost theorem is fully proved and closes the ledger half of that interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.