Jcost_n_zero_iff
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not treat channels with zero or negative values.
- Does not supply convergence rates for gradient flow.
- Does not handle statistical dependence between channels.
- Does not give explicit lower bounds away from the minimum.
formal statement (Lean)
48theorem Jcost_n_zero_iff {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
49 Jcost_n x hx = 0 ↔ ∀ i, x i = 1 := by
proof body
Term-mode proof.
50 unfold Jcost_n
51 constructor
52 · intro h i
53 by_contra hi
54 have hnn : ∀ j : Fin n, 0 ≤ Jcost (x j) := fun j => by
55 by_cases hj : x j = 1
56 · rw [hj, Jcost_unit0]
57 · exact le_of_lt (Jcost_pos_of_ne_one (x j) (hx j) hj)
58 have hle : Jcost (x i) ≤ ∑ j : Fin n, Jcost (x j) :=
59 Finset.single_le_sum (fun j _ => hnn j) (Finset.mem_univ i)
60 linarith [h ▸ hle, Jcost_pos_of_ne_one (x i) (hx i) hi]
61 · intro hall
62 have : ∀ i : Fin n, Jcost (x i) = 0 := fun i => by rw [hall i, Jcost_unit0]
63 simp [this]
64
65/-- J_n is symmetric channel-wise. -/