deficitSourceAction
plain-language theorem explainer
Names the constitutive action for a signed deficit-source coupling: the multi-channel J-cost of exponential strains minus a linear source term. Gravity and ledger auditors cite it as the exact missing premise that bare RecognitionLedgers lack. It is a one-line definitional wrapper around the already-built sourced action, evaluated at the coupling's source strength.
Claim. Given a deficit-source constitutive coupling $C$ on a type $H$, a state $\sigma\in H$, and channel strains $t:\mathrm{Fin}(n)\to\mathbb{R}$ (with $n=C$'s channel count), the constitutive action is the sourced multi-channel action on those $n$ channels at source strength $c_\sigma=\kappa_\sigma\cdot\delta_\sigma$. Equivalently (by the companion identification), $\sum_i J(e^{t_i})-(c_\sigma/n)\sum_i t_i$.
background
This module is the P2.1 terminal blocker for the recognition-ratio bridge: a bare RecognitionLedger does not force the ratio. Coboundary strains telescope on closed cycles, a total-strain budget already assumes the conclusion, and opposite signed sources induce the same bare two-cell J-ledger, so no selector recovers the signed source from bare data alone.
The missing premise is packaged as DeficitSourceConstitutiveCoupling: channel count $n\ge 1$, hinge coupling $\kappa$, signed geometric deficit $\delta$, source strength $c_\sigma=\kappa_\sigma\delta_\sigma$, positive mesh scale, and a structural small-source bound. The action itself is built from the standard Recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $H(x)=J(x)+1=\frac12(x+x^{-1})$ satisfying the d'Alembert form of the RCL).
Upstream cost infrastructure (observer forcing, multiplicative recognizers, rung coarsening) all identify event cost with $J$ on positive ratios. The present definition only wires that cost into the sourced multi-channel action at the coupling's $c_\sigma$; it never mentions $x$-ratios or log-ratio bridges.
proof idea
Definitional one-line wrapper. It applies the existing multi-channel sourced action to the coupling's channel count and to the scalar source strength $C.\mathrm{sourceStrength},\sigma$, leaving the strain vector $t$ as the free field. No tactics, no lemmas, no algebraic reduction beyond that substitution. The companion theorem then unfolds the wrapper and identifies the body with $\sum_i J(e^{t_i})-(c_\sigma/n)\sum_i t_i$.
why it matters
This is the named constitutive action inside the exact missing premise of the recognition-ratio substrate blocker. Downstream, deficitSourceAction_eq_jcost_sum identifies it with summed J-cost minus the linear deficit-source term, "without assuming any ratio relation." That identification lets stationarity of the sourced action derive the recognition-ratio bridge and its cubic remainder once the coupling is supplied, while keeping the positive result non-circular.
In the SevenGaps gravity package this closes the gap between bare ledger data and the sourced J-action used for ratio recovery. It sits downstream of the forcing-chain cost calculus (T5 J-uniqueness and the RCL) and upstream of the nontrivial small-mesh family that shows the sourced construction is uniformly admissible. It does not itself prove the ratio; it only names the action the ratio proof stationarizes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.