sourceCost1_min_le
plain-language theorem explainer
The per-channel sourced recognition cost attains its global minimum at strain equal to arsinh of the source amplitude. Anyone proving universal convergence of cost-decreasing carrier dynamics cites this comparison as the Lyapunov floor. The argument is a two-line case split: equality is reflexive; off the candidate minimizer the sibling strict inequality yields the weak bound.
Claim. For all real $a$ and $t$, if $\Phi_a$ denotes the per-channel sourced cost on strain space, then $\Phi_a(\operatorname{arsinh} a) \le \Phi_a(t)$. Equivalently, $t^*=\operatorname{arsinh} a$ is a global minimizer of $\Phi_a$.
background
This module treats the descent principle for hinge-link strain: the carrier dynamics is steepest descent of total recognition cost, but "steepest" is metric-relative. Part one shows the metric weight $w$ in $\dot t=-w(t)\Phi'(t)$ is not forced by the cost. Part two shows the choice cannot matter: any continuous cost-decreasing map on strain space converges to the same least-cost carrier.
Here $\Phi_a$ (written sourceCost1 a in the development) is the per-channel sourced cost at fixed source amplitude $a$, a real function of the strain coordinate $t$. Sibling calculus facts establish continuity, derivative formulae, coercivity, and one-sided strict monotonicity about $t^=\operatorname{arsinh} a$. The candidate minimizer $t^$ is the unique critical point of the sourced cost (strain balancing the source).
The immediate upstream comparison is the strict inequality off $t^*$: whenever $t\ne\operatorname{arsinh} a$, one has $\Phi_a(\operatorname{arsinh} a)<\Phi_a(t)$. The present statement is the corresponding non-strict global minimum claim used by Lyapunov arguments.
proof idea
Tactic proof by cases on whether $t$ equals $\operatorname{arsinh} a$.
If equal, rewrite the goal; both sides coincide, so $\le$ holds by reflexivity.
If unequal, apply the sibling strict inequality (sourceCost1_lt_of_ne) and pass to the non-strict order via .le. No calculus or coercivity is reopened here; the work is already in the strict comparison.
why it matters
This is the floor inequality for the module's main Lyapunov theorem cost_decreasing_dynamics_converges: any continuous $S$ that strictly spends $\Phi_a$ off $t^=\operatorname{arsinh} a$ and fixes $t^$ has every orbit $S^{[k]}s_0\to t^$. Limit points of cost-nonincreasing orbits must match cost with their image; descent then forces the limit to be $t^$, which is only coherent once $t^*$ is known to be a global minimizer.
In the Seven Gaps gravity stack this closes the gap between "metric is a choice" and "the choice cannot matter": every member of the steepest-descent family (Euclidean weight, Hessian weight $\cosh$, or any other positive $w$), and every other cost-decreasing continuous dynamics, reaches the same sourced least-cost carrier. That carrier is the C2 stationarity target reduced earlier by StrainDescent. No forcing-chain landmark (T5--T8) is invoked directly; the result is pure real analysis on the sourced cost, but it is what makes the descent principle universal rather than metric-dependent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.