Jcost_n_zero_iff
plain-language theorem explainer
Multi-channel J-cost vanishes precisely when every component equals one. Researchers on the ALEXIS B5 empirical program cite the result to certify that the summed cost reaches its global minimum only at the all-ones vector. The argument unfolds the sum definition, applies the single-channel positivity lemma inside a contradiction for the forward direction, and substitutes the unit value for the converse.
Claim. Let $n$ be a natural number and let $x$ be a vector in $R^n$ with every component strictly positive. Then the summed cost $J_n(x) = sum_i J(x_i)$ equals zero if and only if $x_i = 1$ for every index $i$.
background
The module defines the multi-channel J-cost as the sum of single-channel J-costs over $n$ independent positive components. This additive extension matches the ALEXIS Exp B5 run, which treated amplitude, phase, and frequency as separate channels whose costs add.
proof idea
Unfold the sum definition of Jcost_n. The forward direction assumes the total sum is zero, isolates any deviant component via the single-summand inequality, and invokes Jcost_pos_of_ne_one to reach a contradiction. The converse replaces each term by zero using Jcost_unit0 and simplifies the sum.
why it matters
The theorem supplies the zero_iff field of the MultiChannelJCostCert certificate. It completes the uniqueness claim for the multi-channel cost in the ALEXIS B5 formalisation, confirming the all-ones vector as the sole global minimum and supporting the listed descent property. The result aligns with the J-uniqueness step of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.