MultiChannelJCostCert
plain-language theorem explainer
The MultiChannelJCostCert structure packages non-negativity, zero uniqueness, unit-vector evaluation and symmetry for the summed J-cost J_n over n channels. Researchers citing the ALEXIS B5 run or extending Recognition Science to multi-channel costs reference it to confirm the global minimum remains at the all-ones vector. It is realized as a bare structure definition that directly assembles four lemmas already proved for the sum-of-individual-Jcosts function.
Claim. Let $J_n(x) = sum_i J(x_i)$ for $x in R^n_{>0}$. The structure asserts $J_n(x) >= 0$, $J_n(x)=0$ iff $x_i=1$ for all i, $J_n(1)=0$, and $J_n(x)=J_n(x^{-1})$ componentwise.
background
The module introduces the multi-channel J-cost as the direct sum $J_n(x) = sum_i J(x_i)$ for positive real vectors of length n. This additive extension appears in the ALEXIS B5 experiment to treat amplitude, phase and frequency as independent channels whose costs add. The upstream definition Jcost_n supplies the concrete summation, while the module documentation records that the B5 run observed convergence with mean near 1.14 under gradient flow on this cost.
proof idea
The declaration is a structure definition containing no proof body. It records four fields whose values are supplied verbatim by the sibling lemmas Jcost_n_nonneg, Jcost_n_zero_iff, Jcost_n_at_ones and Jcost_n_symm.
why it matters
The structure is instantiated by the downstream definition multiChannelJCostCert, which populates each field with the corresponding lemma. It thereby packages the four properties listed in the module documentation for the ALEXIS B5 formalisation. Within Recognition Science it closes the multi-channel extension of the J-uniqueness step T5, confirming that the summed cost inherits non-negativity and the unique minimizer at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.