Jcost_n_symm
plain-language theorem explainer
The multi-channel J-cost equals its value on the componentwise reciprocal vector. Researchers formalising the ALEXIS B5 experiment cite this invariance to close the symmetry clause of the cost certificate. The proof is a one-line term that unfolds the sum definition and applies the single-channel symmetry lemma to each coordinate.
Claim. Let $J_n(x) := sum_i J(x_i)$ for $x in (R^+)^n$. Then $J_n(x) = J_n(x^{-1})$, where the reciprocal is taken componentwise.
background
The module extends single-channel J-cost to n independent channels by defining J_n as the sum of individual J(x_i). This additive structure appears in the ALEXIS B5 run for amplitude, phase and frequency channels. The upstream lemma Jcost_symm establishes that the base J-cost is unchanged under inversion of its argument, which is the key building block here. From the module documentation, the multi-channel generalisation satisfies four properties: non-negativity, unique minimum at the all-ones vector, symmetry under inversion, and descent under gradient flow.
proof idea
The proof unfolds the definition of Jcost_n to obtain the sum over i of J(x i). Congruence reduces the equality of sums to equality of each term, and extensionality allows application of the single-channel symmetry lemma Jcost_symm to the positivity hypothesis for that coordinate.
why it matters
This result supplies the symmetry field in the multiChannelJCostCert definition, completing the formal certificate for the multi-channel cost. It realises the third key theorem listed in the module documentation for the ALEXIS B5 formalisation. The symmetry is consistent with the fixed-point behaviour at unity that underlies the descent property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.