multiChannelJCostCert
A definition assembles the certificate structure for the multi-channel J-cost by directly assigning its non-negativity, zero-condition at the all-ones vector, evaluation at that point, and inversion symmetry from four supporting lemmas. Researchers formalizing the ALEXIS B5 experiment or multi-channel extensions of the single-channel J-cost would cite it to invoke the complete property bundle at once. The construction is a record literal that references the component theorems without further reasoning steps.
claimThe multi-channel J-cost certificate is the structure asserting non-negativity $0 ≤ J_n(x)$ for positive vectors $x ∈ ℝ^n$, the equivalence $J_n(x) = 0 ↔ x = 1⃗$, the evaluation $J_n(1⃗) = 0$, and symmetry $J_n(x) = J_n(x^{-1})$ componentwise, where $J_n(x) = ∑_i J(x_i)$ and $J$ denotes the single-channel cost function.
background
The module extends the single-channel J-cost to n independent channels via the additive definition $J_n(x) = ∑_i J(x_i)$ for $x ∈ ℝ^n$ with all components positive. This generalization is the formal counterpart of the ALEXIS Exp B5 run, which modeled amplitude-phase-frequency triplets and reported convergence to a mean near unity. The certificate structure packages four properties that the module proves for $J_n$: non-negativity, uniqueness of the global minimum at the all-ones vector, the explicit value zero at that vector, and symmetry under componentwise inversion.
proof idea
The definition is a direct record construction that populates each field of the MultiChannelJCostCert structure by reference to the corresponding sibling theorem: nonneg receives Jcost_n_nonneg, zero_iff receives Jcost_n_zero_iff, at_ones receives Jcost_n_at_ones, and symm receives Jcost_n_symm. No tactics or reductions are applied beyond the record literal itself.
why it matters in Recognition Science
The definition supplies a single certified object that collects the verified properties of the multi-channel J-cost, enabling uniform invocation in any downstream argument that relies on descent, fixed-point uniqueness, or symmetry for the summed cost. It directly implements the key theorems listed in the module documentation for the ALEXIS B5 formalization and extends the single-channel J-uniqueness result to the multi-channel setting while preserving non-negativity and the fixed point at unity. No open questions or scaffolding remain inside the module.
scope and limits
- Does not establish existence or uniqueness of the underlying single-channel J function.
- Does not prove convergence of any gradient flow on J_n.
- Does not treat channels that may take non-positive values.
- Does not supply explicit numerical evaluations of J_n for concrete n or x.
formal statement (Lean)
79def multiChannelJCostCert : MultiChannelJCostCert where
80 nonneg := Jcost_n_nonneg
proof body
Definition body.
81 zero_iff := Jcost_n_zero_iff
82 at_ones := fun _ => Jcost_n_at_ones
83 symm := Jcost_n_symm
84
85end IndisputableMonolith.Foundation.MultiChannelJCost