Foundation Multi Channel Jcost Jcost N At Ones

The single point of rest

A cost function assigns a number to a state, and the state with the lowest cost is the one a system naturally settles into. The multi-channel J-cost extends this idea to several independent channels at once. For a vector of positive numbers x, the multi-channel cost is the sum of the single-channel costs of each entry: J_n(x) = Σᵢ J(xᵢ). The single-channel cost J itself is the proved function J(x) = (x + 1/x)/2 - 1, which is zero exactly when x = 1 and positive otherwise.

The declaration Jcost_n_at_ones establishes the simplest fact about this multi-channel cost: when every channel is set to 1, the total cost is exactly zero. That is, J_n(1, 1, ..., 1) = 0. This is not a deep theorem in itself; it follows directly from the single-channel fact that J(1) = 0. But it is the anchor point for the more substantial result that follows in the same file: the multi-channel cost is zero if and only if every channel is at 1. That equivalence, Jcost_n_zero_iff, is what makes the all-ones vector the unique global minimum of the cost.

The meaning is plain. If each channel measures how far some quantity has drifted from its neutral value, then the whole system rests only when every channel is neutral. No combination of off-balance channels can cancel out to give zero total cost, because each individual cost is non-negative and vanishes only at its own neutral point. The gradient flow on this cost drives any starting configuration toward the all-ones vector, which is the statement that the system seeks its single point of rest.

In Recognition Science, this multi-channel cost models a ledger of independent recognition events. The framework's library, a machine-checked collection of formal theorems, proves these facts with no unproved assumptions. The declaration itself is a theorem, verified in the formal system. What it does not claim is any physical law, any statement about how real systems behave, or any empirical prediction. It is a mathematical fact about a defined function, not a claim about the world.

/-- 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)

/-- The multi-channel fixed point is 1⃗. -/
theorem Jcost_n_at_ones {n : ℕ} :
    @Jcost_n n (fun _ => (1 : ℝ)) (fun _ => one_pos) = 0 := by
  unfold Jcost_n
  simp [Jcost_unit0]

/-- 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]

What this page does not claim

No claim that any physical system actually minimizes this cost. No claim about the rate or path of convergence to the all-ones vector. No claim that the multi-channel cost is the unique cost function satisfying the five conditions.

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: