sourceCost1_continuous
plain-language theorem explainer
For any fixed source strength a, the per-channel sourced cost Φ_a(s) = cosh s − 1 − a·s is continuous in the strain s. Anyone proving monotonicity, coercivity, or Lyapunov convergence for hinge-link strain descent cites this. The proof unfolds the definition and discharges continuity by Mathlib's fun_prop automation on cosh and arithmetic.
Claim. For every real source strength $a$, the map $s \mapsto \cosh s - 1 - a s$ is continuous on $\mathbb{R}$.
background
In the SevenGaps strain-descent setting, the per-channel sourced cost is $\psi_a(s) = \cosh s - 1 - a\cdot s$ (Lean sourceCost1). Its unique minimizer is $t^* = \mathrm{arsinh}, a$, and its residual (gradient) is $\sinh s - a$. This is the scalar cost whose steepest-descent dynamics recovers the sourced least-cost carrier on a hinge link.
The surrounding module asks what the descent principle actually costs once the carrier dynamics is reduced to gradient flow on strain. Part one notes that "steepest" is metric-relative: any positive weight $w$ gives a flow $\dot t = -w(t)\Phi'(t)$ with the same rest point. Part two shows the metric choice is irrelevant: any continuous cost-decreasing map on strain space has every orbit converging to $t^*$.
Continuity of $\Phi_a$ is the elementary analytic input needed before derivative tests, coercivity, and Lyapunov arguments can run.
proof idea
One-line automation after unfolding. Expand sourceCost1 a to $s \mapsto \cosh s - 1 - a s$, then invoke Mathlib fun_prop, which knows continuity of Real.cosh, multiplication by the constant $a$, subtraction, and composition of continuous maps on $\mathbb{R}$. No manual $\varepsilon$-$\delta$ work and no named continuity lemmas beyond the automation database.
why it matters
This is the continuity hinge for the module's Lyapunov package. Downstream, sourceCost1_strictMonoOn and sourceCost1_strictAntiOn feed (sourceCost1_continuous a).continuousOn into strictMonoOn_of_deriv_pos / strictAntiOn_of_deriv_neg on the half-lines about $\mathrm{arsinh}, a$, establishing that cost strictly rises above and falls below the least-cost point.
Those facts, with coercivity, underwrite the main theorem cost_decreasing_dynamics_converges: any continuous dynamics $S$ that strictly spends cost off $t^$ has every orbit $S^{[k]}s_0 \to t^$, with no metric, step size, gradient structure, rate, or convexity of $S$. Continuity of the cost is also used in rest_state_forced, which shows the rest-state hypothesis is not extra: continuous cost-decreasing dynamics must fix $t^*$.
In the broader Recognition gravity story this closes the analytic gap between the C2 stationarity premise and a purely dynamical least-cost carrier, so metric non-uniqueness (part one) cannot spoil convergence (part two).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.