sourcedAction_eq_sum
plain-language theorem explainer
The sourced action on n ticks with coupling c equals the sum of independent per-tick terms cosh(t_i)-1-(c/n)t_i. Authors of the hinge-stationarity bridge cite this to move from the global Phi form to pointwise comparison and uniqueness. The proof unfolds the definition and redistributes the linear coupling across the finite sum via standard Finset identities.
Claim. For any $n \in \mathbb{N}$, coupling $c \in \mathbb{R}$, and tick configuration $t:\{0,\ldots,n-1\}\to\mathbb{R}$, the sourced action equals $\sum_i\bigl(\cosh(t_i)-1-\frac{c}{n}\,t_i\bigr)$.
background
In the Seven Gaps hinge-stationarity core, the honest mechanism for a nonzero hinge deficit is minimization of a sourced action: J-cost of the exponential per-tick strain ratios plus an explicit linear coupling to the deficit. The recognition cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$; on the exponential chart this is $\cosh t-1$ via the kernel identity $J(e^t)=\cosh t-1$.
The module isolates how much of the paper bridge $\log x_\sigma=\kappa_\sigma\delta_\sigma+O(h^3)$ follows from J-stationarity alone, and where a constitutive MODEL coupling enters. The global form is $\Phi(t)=\sum_i(\cosh t_i-1)-(c/n)\sum_i t_i$. This theorem rewrites that global expression as a plain sum of identical per-tick summands, which is the algebra needed for pointwise comparison against the uniform candidate $t_i=\mathrm{arsinh}(c/n)$.
proof idea
One short tactic proof. Unfold the definition of the sourced action (global sum of $\cosh t_i-1$ minus the scaled total $\sum t_i$). Apply Finset.mul_sum to push the scalar $c/n$ inside the sum, then Finset.sum_sub_distrib to combine the two sums into a single sum of per-tick terms $\cosh(t_i)-1-(c/n)t_i$. No analysis or cost lemmas are required; pure finite-sum algebra.
why it matters
This is the bookkeeping hinge between the global sourced action and every pointwise stationarity argument in the module. Global minimality (sourced_minimizer_le) and uniqueness (sourced_minimizer_unique) both rewrite both sides with this identity, then compare termwise via the cosh tangent inequalities. Strain descent reuses it as sourcedAction_eq_sum_sourceCost1 to identify the action with a sum of per-channel source costs. Approximate-minimizer diameter bounds (approx_tick_dist) likewise reduce distance-to-well estimates to the same per-tick decomposition.
In the framework it puts the promotion phrase "derived from an explicit deficit-source constitutive action plus J-stationarity" on a kernel equation: the cost part is identified with summed $J(e^{t_i})$, and only the coupling coefficient remains MODEL. It sits downstream of the kill records for the raw Stokes route and budget circularity, and upstream of the cubic-error ratio $n,\mathrm{arsinh}(c/n)=c+O(c^3)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.