ratioBridge_separates_deficit_observables
plain-language theorem explainer
For every positive d, an exact unit-coupled two-hinge witness carries signed geometric deficits (+d and −d) while the induced recognition ledger has only nonnegative, sign-even deficits. Anyone reconciling the paper's odd log-ratio bridge with the ledger sign and parity no-gos cites this. The proof is a short conjunction of definitional equalities, the two-hinge deficit lemma, ledger nonnegativity, and evenness under d ↦ −d.
Claim. For every real $d>0$, the exact unit-coupled two-hinge witness bridge $B_d$ satisfies: remainder bound $0$; coupling $\kappa_\sigma=1$ at every hinge; geometric deficit $d$ at hinge $0$ and strictly negative geometric deficit at hinge $1$; the induced recognition-ledger deficit is nonnegative at every cell; and that ledger deficit is unchanged when $d$ is replaced by $-d$.
background
Phase 0a of the Seven Gaps program encodes the paper's substrate-to-geometry bridge as an odd relation on a positive comparison ratio $x_\sigma$ at each hinge:
$$\log x_\sigma = \kappa_\sigma,\delta_\sigma + r_\sigma,\qquad |r_\sigma|\le R,h^3.$$
That is an admissibility clause on $\log x$, not an equality of nonnegative deficits. The older form that identified ledger deficit with signed geometric hinge deficit is refuted: ledger deficits are nonnegative and even in the deformation parameter, while signed Regge response is odd.
A RecognitionRatioBridge packages the ratio field, couplings, geometric deficits, mesh scale, and remainder bound. The two-hinge witness family is an exact ($R=0$), unit-coupled ($\kappa=1$) instance with geometric deficits $+d$ and $-d$. The induced ledger is built by feeding the comparison-ratio quotient into the J-cost (equivalently $\cosh(\log x)-1$), realized through the proved coboundary strain ledger. J-cost is the unique cost forced by the Recognition Composition Law (T5).
proof idea
Term-mode refine assembles a six-way conjunction. Remainder bound and unit coupling are definitional (rfl). Geometric deficit at hinge 0 is the first half of twoHingeWitnessBridge_deficit d. Negativity at hinge 1 rewrites by the second half of that lemma and finishes with linarith against $d>0$. Nonnegativity of the induced ledger deficit is RecognitionLedger.deficit_nonneg at each cell. Evenness under $d\mapsto -d$ is twoHingeWitness_ledger_deficit_even d. No new algebra is invented here; the witness and ledger lemmas do the work.
why it matters
This is the kernel-checked reconciliation: the no-gos constrain the ledger deficit, while the paper's odd bridge stores signed information in $\log x$ (hence in the geometric deficit). The two observables are separated on an explicit witness, so the no-gos and the paper bridge are jointly consistent.
Downstream, ratioBridge_jcost_quadratic_inexact expands the bridge J-cost to quadratic order with controlled remainder; stationarity closure uses the same witness family for concreteStationarityBridge_nonvacuous (signed $\pm 1/16$ deficits, non-vacuous negative hinge) and for ofStationarity_minimizer_grounding (ratio field pinned as the unique global minimizer of the sourced action). In the forcing chain this sits under T5 J-uniqueness: ledger cost sees only the even part $J(x)=\cosh(\log x)-1$, while the odd content lives in $\log x$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.