constrained_equal_split
plain-language theorem explainer
Under a fixed budget sum of real strains equal to c, the summed J-cost sum_i (cosh t_i - 1) is at least n(cosh(c/n)-1), so the equal split is optimal on that constraint set. Hinge-stationarity and sourced-ratio arguments in the Seven Gaps gravity bridge cite this constrained lower bound. The proof sums the cosh tangent-line inequality at c/n; linear remainders cancel against the budget.
Claim. For every natural number $n\ge 1$, every real budget $c$, and every real family $(t_i)_{i\in\{1,\ldots,n\}}$ with $\sum_i t_i=c$, one has $n\bigl(\cosh(c/n)-1\bigr)\le\sum_i\bigl(\cosh t_i-1\bigr)$.
background
In Recognition Science the elementary cost is $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$. On a hinge the working variables are log-strains $t_i$, so the summed cost is $\sum_i(\cosh t_i-1)$. Convexity of cosh is the analytic engine.
This module records how much of the paper bridge $\log x_\sigma=\kappa_\sigma\delta_\sigma+O(h^3)$ follows from pure J-cost stationarity, and where a constitutive model input must enter. Two kill records already closed the raw Stokes route (coboundary strains telescope to zero on closed cycles) and the circular-budget route (imposing $\sum t_i=\kappa\delta$ already is the ratio conclusion).
The local analytic prior is the tangent-line bound: for all real $u,t$, $\cosh u+\sinh u\cdot(t-u)\le\cosh t$. That supporting-line inequality is summed here at the common basepoint $u=c/n$.
proof idea
Fix the basepoint $u=c/n$. Apply the cosh tangent-line bound at that $u$ to each coordinate $t_i$, then sum over $i$. The left-hand side is $\sum_i\bigl(\cosh(c/n)+\sinh(c/n)(t_i-c/n)\bigr)$.
Rewrite each summand as a constant piece plus $\sinh(c/n)\cdot t_i$. The constant pieces sum to $n$ times a fixed expression; the linear pieces become $\sinh(c/n)\cdot\sum_i t_i$. The budget $\sum_i t_i=c$ cancels the remainder and leaves exactly $n\cosh(c/n)$.
Rewrite the target right-hand side as $\sum_i\cosh t_i-n$, substitute the simplified left-hand side into the summed inequality, and finish by linear arithmetic. No uniqueness or stationarity step is used: pure convexity plus budget cancellation.
why it matters
This is item 5 of the hinge-stationarity core: the constrained lower bound that makes equal split optimal under a fixed holonomy budget. The companion equality characterization (minimum attained iff every $t_i=c/n$) sits immediately downstream in the same module. Together they form the constrained half of the sourced stationary-ratio story; the unconstrained half minimizes $\Phi(t)=\sum_i(\cosh t_i-1)-(\kappa\delta/n)\sum_i t_i$ and obtains the unique minimizer $t_i=\mathrm{arsinh}(\kappa\delta/n)$ with cubic error $1/6$.
The module stresses the honest reading: the theorem extracts the equal-split value from a budget already given; it does not, and cannot, produce the budget itself (that circularity is the kill record behind the sibling budget-implies-ratio statement). In the broader RS gravity program this is the analytic content of equal-split optimality for J-cost on a hinge with fixed total strain, independent of Regge mesh geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.