Foundation Multi Channel Jcost Jcost N Nonneg

The nonnegative cost

In mathematics, a cost function assigns a number to a state, often measuring how far that state is from a preferred one. The Recognition Science framework uses a specific cost function, J(x) = (x + 1/x)/2 - 1, which is zero when x equals 1 and grows as x moves away from 1 in either direction. The declaration Jcost_n_nonneg extends this idea from a single number to a whole list of positive numbers, one per independent channel, and proves a basic fact about the extension: the total cost is never negative.

The extension is defined by adding up the individual costs. If you have n channels with values x₁, x₂, ..., xₙ, the multi-channel cost J_n(x) is simply J(x₁) + J(x₂) + ... + J(xₙ). Since each J(xᵢ) is nonnegative, their sum is nonnegative. The theorem Jcost_n_nonneg states this formally: for any finite list of positive numbers, the sum of their individual J-costs is greater than or equal to zero. The proof in the machine-checked library of formal theorems proceeds by showing each term in the sum is nonnegative, using the fact that J(x) is nonnegative for all positive x.

The theorem is one of four properties that together characterize the multi-channel extension. The others, also proved in the same library, state that the total cost is zero exactly when every channel sits at its equilibrium value of 1, that the cost is symmetric under replacing every value by its reciprocal, and that the all-ones vector is a fixed point. These four properties are bundled into a structure called MultiChannelJCostCert, which acts as a certificate that the extension behaves as intended.

In Recognition Science, this multi-channel version models situations where several independent quantities must each be recognized simultaneously. The nonnegativity result guarantees that the total cost never dips below zero, which is a sanity condition for any cost function. It does not, however, say anything about how fast the cost decreases, whether a minimum is actually reached, or what the physical meaning of the channels might be. Those questions remain open or are handled by other parts of the framework.

/-- Multi-channel J-cost: sum of individual J-costs. -/
noncomputable def Jcost_n {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) : ℝ :=
  ∑ i, Jcost (x i)

/-- J_n ≥ 0. -/
theorem Jcost_n_nonneg {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
    0 ≤ Jcost_n x hx := by
  unfold Jcost_n
  apply Finset.sum_nonneg
  intro i _
  by_cases h : x i = 1
  · simp [h, Jcost_unit0]
  · exact le_of_lt (Jcost_pos_of_ne_one (x i) (hx i) h)

/-- J_n = 0 iff all channels at equilibrium. -/
theorem Jcost_n_zero_iff {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
    Jcost_n x hx = 0 ↔ ∀ i, x i = 1 := by
  unfold Jcost_n
  constructor
  · intro h i
    by_contra hi
    have hnn : ∀ j : Fin n, 0 ≤ Jcost (x j) := fun j => by
      by_cases hj : x j = 1
      · rw [hj, Jcost_unit0]
      · exact le_of_lt (Jcost_pos_of_ne_one (x j) (hx j) hj)
    have hle : Jcost (x i) ≤ ∑ j : Fin n, Jcost (x j) :=
      Finset.single_le_sum (fun j _ => hnn j) (Finset.mem_univ i)
    linarith [h ▸ hle, Jcost_pos_of_ne_one (x i) (hx i) hi]
  · intro hall
    have : ∀ i : Fin n, Jcost (x i) = 0 := fun i => by rw [hall i, Jcost_unit0]
    simp [this]

/-- J_n is symmetric channel-wise. -/
theorem Jcost_n_symm {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
    Jcost_n x hx = Jcost_n (fun i => (x i)⁻¹) (fun i => inv_pos.mpr (hx i)) := by
  unfold Jcost_n
  congr 1; ext i; exact Jcost_symm (hx i)

What this page does not claim

Jcost_n_nonneg does not claim that the multi-channel cost reaches a minimum, only that it never goes below zero. The theorem does not assign any physical meaning to the channels; it is a purely mathematical statement about the defined function. The nonnegativity result does not by itself force the all-ones vector to be the unique global minimum; that requires the separate zero_iff theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/MultiChannelJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: