sourcedMinimizer
plain-language theorem explainer
Uniform strain configuration sending every tick index to arsinh(c/n), the claimed unique global minimizer of the sourced hinge action. Gravity bridge and recognition-ratio derivations cite it as the stationary point of J-cost plus deficit-source coupling. Defined as the constant Fin-n map; uniqueness and global minimality are proved separately.
Claim. For $n \in \mathbb{N}$ and source strength $c \in \mathbb{R}$, the sourced minimizer is the constant map $t:\{0,\ldots,n-1\}\to\mathbb{R}$ with $t_i=\operatorname{arsinh}(c/n)$ for every tick index $i$.
background
This module isolates how much of the paper bridge $\log x_\sigma=\kappa_\sigma\delta_\sigma+O(h^3)$ follows from J-cost stationarity alone, versus where a constitutive model input must enter. The honest mechanism is the sourced action $$\Phi(t)=\sum_i(\cosh t_i-1)-(c/n)\sum_i t_i,$$ i.e. summed J-cost of exponential strain ratios minus an explicit deficit-source coupling linear in the strains.
The cost term $\cosh t-1$ is the T5 J-cost $J(e^t)$ (equivalently $\cosh(\log x)-1$). Stationarity of each summand forces $\sinh t_i=c/n$, hence $t_i=\operatorname{arsinh}(c/n)$. The raw Stokes and circular budget routes are already killed in-module; this definition names the candidate that the sourced route actually uses.
Upstream constants only supply the tick quantum $\tau_0=1$ and an independence predicate on coupled axes; neither shapes the formula beyond the ambient RS ledger setting.
proof idea
Pure definition: the constant function on Fin n with value Real.arsinh (c / n) at every index. No proof obligations. Downstream lemmas (sourced_pointwise_le, sum decomposition of the action) turn this ansatz into global minimality and uniqueness.
why it matters
Names the unique global minimizer that the sourced-stationary-ratio story needs. Immediate parents: sourced_minimizer_le (global minimality over all configurations), sourced_minimizer_unique (any minimizer equals this map), and their package sourced_unique_minimizer. Also feeds sourcedValue_eq_action_min (optimal value equals action at this point), the recognition-ratio derivation half (recognition_ratio_derived / recognition_ratio_derived_holds), the blocker identity equating log-ratio to minimizer strain, and descent universality (link_channels_converge: cost-decreasing dynamics on each channel rest at this value).
In the Seven Gaps panel this is the constructive core of the honest mechanism after kill records C6 (raw Stokes) and raw 1b (budget circularity). It converts J-stationarity into the forced relation $n,\operatorname{arsinh}(c/n)=c+O(c^3)$ with explicit cubic constant, which is the bridge content actually derived rather than posited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.