Jcost_n
plain-language theorem explainer
The multi-channel J-cost sums the single-channel J-costs over n independent positive real channels. Researchers working on the ALEXIS B5 experiment or multi-channel extensions in Recognition Science would cite this definition as the starting point for proving non-negativity, uniqueness of the minimum at the all-ones vector, and symmetry. The definition is a direct sum, making all subsequent properties follow immediately from the corresponding single-channel facts.
Claim. For $n ∈ ℕ$ and a vector $x : Fin n → ℝ$ with $x_i > 0$ for all $i$, the multi-channel J-cost is $J_n(x) := ∑_{i} J(x_i)$, where $J$ denotes the single-channel J-cost.
background
The module formalises the multi-channel extension used in the ALEXIS Exp B5 run, where the total cost is the sum of per-channel J-costs for amplitude, phase, and frequency triplets. The single-channel J-cost $J(x)$ satisfies $J(x) ≥ 0$ with equality only at $x=1$, and is symmetric under $x ↔ 1/x$. This definition extends that additively to vectors in $(ℝ^+)^n$. No upstream lemmas are required beyond the import of Jcost from the Cost module.
proof idea
The definition is a one-line wrapper that applies the summation operator to the single-channel Jcost function over the finite index set Fin n.
why it matters
This definition is the foundation for the MultiChannelJCostCert structure and the theorems Jcost_n_nonneg, Jcost_n_zero_iff, Jcost_n_symm, and Jcost_n_at_ones. It directly implements the ALEXIS B5 generalisation $J_n(x) = Σ J(x_i)$, enabling descent arguments and fixed-point analysis in the Recognition Science framework. It supports the extension of the J-uniqueness property to multiple channels without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.