ratioBridgeFromDeficitSourceCoupling
plain-language theorem explainer
From a signed deficit-source constitutive coupling on hinges, build the recognition-ratio bridge whose ratio field is the unique global minimizer of the deficit-source J-action. Gravity workers on the Seven Gaps P2.1 blocker cite this as the positive construction once the missing premise is supplied. The body is a thin wrapper that feeds the coupling data into the stationarity bridge builder, with source domination rewritten via the constitutive identity.
Claim. Given a signed deficit-source constitutive coupling $C$ on a hinge type $H$ (channel count $n\ge 1$, hinge couplings $\kappa$, geometric deficits $\delta$, source strengths satisfying $c_\sigma=\kappa_\sigma\,\delta_\sigma$, and mesh scale $h>0$ with the structural small-source bound), produce the recognition-ratio bridge on $H$ obtained from J-stationarity of the deficit-source action.
background
Module P2.1 is the terminal blocker for the recognition-ratio gap in gravity: a bare recognition ledger does not force the ratio bridge. Coboundary strains telescope on cycles, an imposed total-strain budget is circular, and opposite signed sources induce the same bare two-cell J-ledger, so no selector from bare ledgers recovers the signed source.
The missing premise is the structure DeficitSourceConstitutiveCoupling: channel count, hinge coupling $\kappa$, signed geometric deficit, source strength tied by $c_\sigma=\kappa_\sigma,\delta_\sigma$, positive mesh scale, and a structural small-source domination bound. None of these fields mentions the ratio $x$ or $\log x$.
The cost side uses the standard RS J-cost (equivalently the shifted $H(x)=J(x)+1=\frac12(x+x^{-1})$ satisfying the d'Alembert form of the Recognition Composition Law). The bridge constructor invoked here is the stationarity package from the imported StationarityBridgeClosure module: unique global minimizer of the sourced action yields the ratio field and the cubic remainder bound.
proof idea
Definitional one-line wrapper. Unpack the constitutive coupling and pass its channels, positivity, $\kappa$, geometric deficit, and mesh data to recognitionRatioBridge_ofStationarity. The source-strength argument is the pointwise map $\sigma\mapsto c_\sigma$; the proof rewrites via the constitutive identity $c_\sigma=\kappa_\sigma,\delta_\sigma$ and applies the coupling's source_dominated bound. No new analysis is done here; the ratio relation and remainder constant $n/6$ are inherited from the stationarity builder (via stationaryRatio_cubic).
why it matters
This is the positive half of the P2.1 terminal package. After the named coupling is supplied, J-stationarity derives the recognition-ratio bridge without assuming anything about $x$ or $\log x$ in the premise. Downstream, recognition_ratio_derived_of_deficit_source_coupling reads off the cubic bound
$$|\log x_\sigma-\kappa_\sigma,\delta_\sigma|\le (n/6),h^3,$$
and deficitSourceCoupling_logRatio_eq_minimizer_strain identifies $\log x_\sigma$ with the total strain of the unique sourced minimizer. Both feed the proposition-valued RecognitionRatioSubstrateBlockerCertificate, which packages the exact blocker (telescope, circularity, no bare-ledger selector, positive sourced derivation, nontrivial small-mesh family).
In the broader RS gravity chain this closes the substrate gap between bare ledger data and the ratio bridge used in sourced strain bookkeeping; it does not itself touch T5–T8 or the alpha band, but it is the constitutive hinge those continuum limits need once discrete strain is sourced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.