sourced_pointwise_le
plain-language theorem explainer
For every real source strength a, the map t ↦ cosh t − 1 − a·t attains its global minimum at t = arsinh a. Hinge-stationarity and sourced-action arguments in the gravity Seven Gaps stack cite this one-variable bound when reducing multi-tick configurations to the uniform well. The proof is a short term argument: apply the cosh tangent-line inequality at u = arsinh a, cancel sinh(arsinh a) = a, and finish by linear arithmetic.
Claim. For all real $a$ and $t$, $\cosh(\operatorname{arsinh} a) - 1 - a\cdot\operatorname{arsinh} a \le \cosh t - 1 - a\cdot t$. Equivalently, $t \mapsto \cosh t - 1 - a t$ attains its global minimum at $t = \operatorname{arsinh} a$ (where $\sinh t = a$).
background
In the Seven Gaps hinge-stationarity core, the sourced action couples J-cost to an explicit deficit-source term. Recognition J-cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$; on the additive strain coordinate $t$ the cost piece is $\cosh t-1$. The one-variable model functional is therefore $\Phi_a(t)=\cosh t-1-a\cdot t$. The module isolates how much of the paper bridge $\log x_\sigma=\kappa_\sigma\delta_\sigma+O(h^3)$ follows from pure J-cost stationarity versus constitutive model input, after killing the raw Stokes and circular-budget routes.
The upstream tangent-line bound states that for all $u,t$ one has $\cosh u+\sinh u\cdot(t-u)\le\cosh t$: the graph of $\cosh$ lies above every tangent. Specializing the contact point to $u=\operatorname{arsinh} a$ inserts the source strength into the slope via $\sinh(\operatorname{arsinh} a)=a$, which is the first-order stationarity condition for $\Phi_a$.
proof idea
Instantiate the cosh tangent-line inequality at contact point $u=\operatorname{arsinh} a$ and free variable $t$. Rewrite $\sinh(\operatorname{arsinh} a)=a$ to obtain
$\cosh(\operatorname{arsinh} a)+a\cdot(t-\operatorname{arsinh} a)\le\cosh t$.
Rearrange by subtracting $1+a\cdot t$ (discharged by nlinarith) to get the claimed pointwise lower bound of $\Phi_a$ at $\operatorname{arsinh} a$ versus any $t$. Three-line term proof: have the tangent bound, rw the inverse-sinh identity, nlinarith.
why it matters
This pointwise bound is the atomic comparison behind global minimality of the uniform sourced configuration. The parent sourced_minimizer_le sums it over Fin n to show $t_i=\operatorname{arsinh}(c/n)$ minimizes the multi-component sourced action; uniqueness and approximate-minimizer diameter control (sourced_minimizer_unique, approx_tick_dist) reuse the same inequality. In the Recognition framework this is the honest mechanism replacing the killed raw Stokes and circular budget routes: minimizing $\sum_i(\cosh t_i-1)-(c/n)\sum_i t_i$ forces the unique stationary ratio $n\cdot\operatorname{arsinh}(c/n)=c+O(c^3)$, feeding the cubic-error bridge toward the paper relation. It operationalizes J-cost stationarity (forcing landmark T5) at the hinge without importing mesh geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.