mesh_recognition_ratio_derived
plain-language theorem explainer
On the assembled mesh dual-entry deficit-source constitutive coupling, log of the bridge x-ratio stays within an O(meshScale³) envelope of kappa times geometric deficit. Gravity analysts on the Gap-1 residual chain cite this as the conditional recognition-ratio bound for that coupling. Proof is a one-line specialization of the general deficit-source coupling ratio lemma.
Claim. For every real $\sigma$, $\bigl|\log\bigl(x_{\mathrm{ratio}}(\sigma)\bigr) - \kappa(\sigma)\,\Delta_{\mathrm{geom}}(\sigma)\bigr| \le (N_{\mathrm{ch}}/6)\, s^{3}$, where $x_{\mathrm{ratio}}$ is the ratio-bridge map of the mesh dual-entry coupling, $\kappa$ and $\Delta_{\mathrm{geom}}$ are its hinge-kappa and geometric-deficit fields, $N_{\mathrm{ch}}$ its channel count, and $s$ its mesh scale.
background
This module is Wave B residual R4 in the QG Gap-1 residual DAG. It packages three banked pieces into an inhabited deficit-source constitutive coupling on the real carrier: R1 mesh geometric deficit, R2 mesh hinge kappa with source-dominated control, and R3 dual-entry strain state. Premise fields of the coupling are free of x-ratio and log; those appear only in the derived-ratio conclusion.
The recognition-ratio relation compares the logarithm of a bridge ratio to the product of constitutive kappa and geometric deficit, with error at most channels/6 times mesh scale cubed. The general lemma recognition_ratio_derived_of_deficit_source_coupling already proves that bound for any such coupling; the dual-entry mesh object is the concrete instance assembled here.
Convention: deficit means debit-leads (positive hinge), matching the Regge convention pin for the mesh geometric deficit. Carrier is reshaped $H=\mathbb{R}$ from R1/R2, not an encoded Freudenthal triangulation.
proof idea
One-line term proof: apply the general lemma recognition_ratio_derived_of_deficit_source_coupling to the assembled mesh dual-entry coupling at the given real parameter $\sigma$. No local algebra; once the coupling is inhabited, the blocker lemma discharges the absolute-value bound on log-ratio versus kappa times geometric deficit.
why it matters
Closes the R4 step of Wave B on the typed residual that builds a deficit-source constitutive coupling from enrichment: the assembled dual-entry coupling satisfies the conditional recognition-ratio inequality. Doc-comment is explicit that this is not the ledger-named standalone recognition-ratio binding (R5) and does not flip gap1_bridge_derived (R6 still needs R0a, R0b, and R5).
No downstream consumers are wired yet (used_by empty); sibling residual and status declarations in the same module are the immediate neighborhood. R0a/R0b validation name-bindings remain open, and the encoded Freudenthal lift stays open upstream. In the RS gravity stack this is local mesh analysis toward Gap-1 residual closure, not a T0–T8 forcing step or a constants-band claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.