twoHingeWitnessBridge
plain-language theorem explainer
Explicit two-hinge recognition-ratio bridge with geometric deficits $d$ and $-d$, unit coupling, mesh scale 1, and zero remainder. Anyone citing the escape from the ledger sign no-go or the deficit-observable separation uses this witness. The construction assigns $x_\sigma=\exp(\delta_\sigma)$ fieldwise; the exact log-ratio identity is a one-line simplification.
Claim. For every real $d$, the two-hinge data $x_0=e^{d}$, $x_1=e^{-d}$, $\kappa\equiv 1$, $\delta_0=d$, $\delta_1=-d$, mesh scale $h=1$, and remainder bound $0$ form a recognition-ratio bridge on $\{0,1\}$: each $x_\sigma>0$ and $\log x_\sigma=\kappa_\sigma\,\delta_\sigma$ holds exactly (remainder zero).
background
The module encodes the paper's Def 6.2 recognition-ratio admissibility clause: at each hinge $\sigma$ one has a positive comparison ratio $x_\sigma$, a coupling $\kappa_\sigma$, and a signed geometric deficit $\delta_\sigma$, linked by
$$\log x_\sigma=\kappa_\sigma,\delta_\sigma+R_\sigma,\qquad |R_\sigma|\le C,h^3.$$
This is an odd relation on $\log x$, not an equality of nonnegative ledger deficits. The older bridge form (ledger deficit equals signed geometric deficit) was refuted: ledger deficits are nonnegative and even in the deformation parameter, while signed Regge response is odd.
RecognitionRatioBridge packages the new clause as an explicit MODEL-tier hypothesis (not yet derived). The present definition supplies the canonical exact, unit-coupled instance on two hinges that the escape and separation theorems instantiate.
proof idea
Field-by-field structure inhabitant, not a tactic proof. Comparison ratios are $\exp$ of the signed deficits, so positivity is Real.exp_pos. Couplings are constantly 1; mesh scale is 1; remainder bound is 0 with le_refl. The admissibility obligation reduces, after Real.log_exp, to $|0|\le 0$, discharged by one_mul, sub_self, abs_zero, zero_mul, and le_refl.
why it matters
This is the concrete witness behind the module's kernel-checked reconciliation with the no-gos. ratioBridge_admits_negative_deficit packages it as: for every $d$ there exists an exact, unit-coupled bridge with $\delta_0=d$ and $\delta_1=-d$ (strictly negative when $d>0$), impossible for the old deficit-equality form. ratioBridge_separates_deficit_observables then shows the induced ledger deficit stays nonnegative and even under $d\mapsto -d$, while the geometric deficit remains signed: two observables, no contradiction.
Downstream, twoHingeWitnessBridge_xRatio_neg and twoHingeWitness_ledger_deficit_even feed the parity arguments, and the enrichment path (enrichedWitness_toBare) identifies the bare shadow with the sign-blind ledger built from $\log\circ x$. Within Seven Gaps Phase 0a this closes the "odd form escapes the sign obstruction" claim without free fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.