Jcost_n_nonneg
plain-language theorem explainer
The multi-channel J-cost J_n(x) equals the sum of single-channel J-costs over n positive real components and is always non-negative. Researchers formalizing the ALEXIS B5 run or descent arguments in Recognition Science cite this when establishing the global minimum at the all-ones vector. The proof is a direct term-mode argument that unfolds the sum definition and applies non-negativity of each term via case analysis on equality to one.
Claim. Let $n$ be a natural number and let $x$ map the finite set of size $n$ into the reals with every component strictly positive. Then $0$ is a lower bound for $J_n(x)$, where $J_n(x) := sum_i J(x_i)$ and $J$ is the single-channel J-cost.
background
The multi-channel J-cost is defined by the sibling declaration Jcost_n as the sum of individual J-costs: $J_n(x) = sum_i J(x_i)$ for $x$ in $R^n$ with all entries positive. This additive extension appears in the module setting for the ALEXIS B5 formalisation, whose module doc lists four key theorems beginning with non-negativity. The upstream lemmas Jcost_unit0 and Jcost_pos_of_ne_one supply the base facts: Jcost 1 equals zero while Jcost x is strictly positive for x positive and unequal to one.
proof idea
The argument unfolds Jcost_n to expose the finite sum, then applies Finset.sum_nonneg. For each index it branches on whether the component equals one: the equality case invokes Jcost_unit0 to obtain zero, while the inequality case invokes Jcost_pos_of_ne_one to obtain a strict positive lower bound.
why it matters
This theorem supplies the nonnegativity field of the downstream MultiChannelJCostCert, which packages the four properties needed for the multi-channel fixed-point analysis. It closes the first item in the module's listed key theorems and aligns with the Recognition Science forcing chain at T5 J-uniqueness together with the descent dynamics on the phi-ladder. No open scaffolding remains on this point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.