Jcost_n
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.
claimFor $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 in Recognition Science
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.
scope and limits
- Does not establish non-negativity of the sum.
- Does not prove that the sum vanishes only when every component equals one.
- Does not address convergence of gradient flow on the multi-channel cost.
- Does not specify the explicit form of the single-channel Jcost.
Lean usage
theorem Jcost_n_at_ones {n : ℕ} : Jcost_n (fun _ => (1 : ℝ)) (fun _ => one_pos) = 0 := by unfold Jcost_n; simp [Jcost_unit0]formal statement (Lean)
28noncomputable def Jcost_n {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) : ℝ :=
proof body
Definition body.
29 ∑ i, Jcost (x i)
30
31/-- J_n ≥ 0. -/