sourced_unique_minimizer
plain-language theorem explainer
For every tick count n and source strength c, the sourced hinge action Φ(t)=Σ(cosh t_i-1)-(c/n)Σ t_i has unique global minimizer t_i=arsinh(c/n). Bridge and gravity authors cite it as the non-circular stationarity mechanism that forces the recognition ratio from J-cost plus an explicit deficit-source coupling. The proof is a one-line term pairing of the lower-bound and uniqueness lemmas.
Claim. For every $n\in\mathbb{N}$, every source strength $c\in\mathbb{R}$, and every configuration $t:\{0,\ldots,n-1\}\to\mathbb{R}$, the sourced action $\Phi_c(t)=\sum_i(\cosh t_i-1)-(c/n)\sum_i t_i$ satisfies $\Phi_c(t^*)\le\Phi_c(t)$ at the constant configuration $t^*_i=\mathrm{arsinh}(c/n)$, and equality $\Phi_c(t)=\Phi_c(t^*)$ forces $t=t^*$.
background
This module isolates how much of the paper bridge relation $\log x_\sigma=\kappa_\sigma\delta_\sigma+O(h^3)$ follows from J-cost stationarity alone, and where a constitutive MODEL input must enter. The J-cost is $J(x)=\cosh(\log x)-1$ (equivalently $(x+x^{-1})/2-1$), forced uniquely by the Recognition Composition Law in the T5 step of the forcing chain. On exponential strain ratios the summed J-cost becomes $\sum_i(\cosh t_i-1)$.
The sourced action adds an explicit linear coupling of total source strength $c$ (standing for $\kappa\delta$) against the total strain: $\Phi(t)=\sum_i(\cosh t_i-1)-(c/n)\sum_i t_i$. The coupling term is flagged MODEL; everything else is theorem. Sibling lemmas already kill the raw Stokes route (coboundary strains telescope to zero on closed cycles) and the circular raw-1b budget route (the budget hypothesis already is the claimed ratio).
The candidate minimizer is the constant field $t_i=\mathrm{arsinh}(c/n)$, whose stationarity condition $\sinh t_i=c/n$ is forced by unconstrained minimization of $\Phi$, not by imposing a holonomy budget a priori.
proof idea
One-line term proof: pair the two already-proved conjuncts. The first component is the global lower bound sourced_minimizer_le, which shows $\Phi(t^*)\le\Phi(t)$ for every configuration $t$. The second is uniqueness sourced_minimizer_unique, which upgrades equality of actions to pointwise equality of configurations. No further calculus or case splits appear at this wrapper; both ingredients live as siblings in the same module.
why it matters
This is item 3 of the hinge-stationarity core: the honest mechanism that replaces the killed raw Stokes and circular budget routes. Downstream, ofStationarity_minimizer_grounding re-exports it for the constructed bridge, pinning the ratio field as the unique global minimizer of the constitutive action. ofStationarity_log_xRatio_eq_minimizer_strain then identifies $\log x_\sigma$ with the total strain of that minimizer, so the ratio is defined from stationarity rather than posited.
The cubic bridge bound stationaryRatio_cubic (T1) expands $n,\mathrm{arsinh}(c/n)=c+O(c^3)$ under the mesh domination $|c|\le n h$, giving $|\log x^*-c|\le(n/6)h^3$. Approximate-minimizer diameter control (sourced_minimizer_sup_diameter) and the mesh-indexed RecognitionRatioFamily also rest on uniqueness of this stationary point. Within the broader RS gravity program it is the local analytic engine behind the sourced stationary ratio, not a claim about D=3 or the eight-tick octave themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.