DeficitSourceConstitutiveCoupling
plain-language theorem explainer
Names the exact missing premise for deriving the recognition-ratio bridge: a signed source strength equal to hinge coupling times geometric deficit, plus a positive mesh scale and a channel-wise small-source bound. Gravity and ledger auditors cite it when showing a bare RecognitionLedger is insufficient. It is a pure structure (model), not a proved claim; fields deliberately omit any ratio or log-ratio data.
Claim. A deficit-source constitutive coupling on a type $H$ consists of a positive channel count $n\ge 1$, maps $\kappa,\delta,c:H\to\mathbb{R}$ with $c(\sigma)=\kappa(\sigma)\,\delta(\sigma)$ for every $\sigma$, a mesh scale $h>0$, and the bound $|c(\sigma)|\le n\,h$ for all $\sigma$. No field refers to a recognition ratio or its logarithm.
background
Module P2.1 isolates why recognition_ratio_derived fails on a bare recognition ledger. Coboundary strains cancel on closed cycles; a total-strain budget already smuggles in the ratio conclusion; and opposite signed sources induce the same two-cell J-ledger, so no bare-ledger selector recovers the signed source.
The J-cost (and its shift $H(x)=J(x)+1=\tfrac12(x+x^{-1})$) is the unique cost forced by the Recognition Composition Law. Upstream cost definitions (observer events, multiplicative recognizers, PRC ratios, rung-coarsened multisets) all reduce to summing that J-cost on positive ratios. The constitutive coupling below never mentions those ratios: it only packages source data and the linear coupling that will later enter the sourced action.
Local setting: after this model is supplied, J-stationarity of the sourced action derives the ratio bridge with cubic remainder; without it the bare ledger is an exact blocker, not a status flag.
proof idea
No proof: this is a structure definition. Fields record channel count with positivity, the three maps $\kappa$, geometric deficit, and source strength linked by the pointwise product law, a strictly positive mesh scale, and the uniform bound $|\mathrm{source}|\le n\cdot h$ used by the cubic estimate. Downstream defs build the sourced action and the stationarity bridge from these fields alone.
why it matters
This is the named missing premise of the Recognition Ratio Substrate Blocker (P2.1). Downstream, deficitSourceAction forms the constitutive action (summed J-cost minus linear source-strain coupling); deficitSourceAction_eq_jcost_sum identifies that action in the kernel without assuming any ratio; ratioBridgeFromDeficitSourceCoupling and recognition_ratio_derived_of_deficit_source_coupling then obtain the bridge with remainder $n/6,h^3$ by J-stationarity alone; deficitSourceCoupling_logRatio_eq_minimizer_strain equates $\log x_\mathrm{ratio}$ to total minimizer strain.
In the Seven Gaps ledger it feeds the substrate-blocker certificate and the broader gravity gap accounting. Framework-wise it sits under the forced J-cost (T5) and the stationarity route to the recognition ratio: the positive result does not assume the bridge, it derives it once the source coupling is present. The metric-carrier gap (P2.5) remains a separate open continuum issue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.