Jcost_n_at_ones
plain-language theorem explainer
The multi-channel J-cost vanishes when every channel input equals one. Equilibrium analysts in Recognition Science cite this to confirm the global minimum of the summed cost function. The proof is a one-line term wrapper that unfolds the sum and applies the single-channel unit lemma.
Claim. For any natural number $n$, let $J_n(x) = sum_{i=1}^n J(x_i)$ where each $x_i > 0$. Then $J_n(1,1,…,1) = 0$.
background
The module defines the multi-channel extension Jcost_n x hx := sum_i Jcost (x i) for a vector x in R^n with all components positive. This additive form matches the ALEXIS B5 experiment description of total cost as the sum over amplitude, phase, and frequency channels. The upstream lemma Jcost_unit0 states that Jcost(1) = 0 by direct simplification of the squared-ratio expression for single-channel J.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of Jcost_n to expose the finite sum of individual Jcost terms, then simplifies each term via the fact that Jcost(1) = 0.
why it matters
This supplies the at_ones field inside the MultiChannelJCostCert record that bundles non-negativity, zero-iff, symmetry, and fixed-point properties. It completes the equilibrium characterization at the unit vector in the Foundation layer, consistent with the Recognition Science fixed-point analysis where J reaches its global minimum at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.