Foundation Multi Channel Jcost Jcost N Symm

The multi-channel ledger

In Recognition Science, the ledger, a discrete record of recognition events, assigns a cost to each event. The single-channel cost function J(x) = (x + 1/x)/2 - 1 measures the price of a recognition when the recognized value is x, with the minimum cost of zero occurring exactly at x = 1. The declaration Jcost_n_symm extends this picture to multiple independent channels, such as the amplitude, phase, and frequency of a signal, by summing the individual costs: J_n(x) = Σᵢ J(xᵢ) for a vector x with all positive entries.

The theorem states that this multi-channel cost is symmetric under componentwise inversion: J_n(x) = J_n(x⁻¹), where x⁻¹ means taking the reciprocal of each entry. In plain terms, if you replace every channel's value by its reciprocal, the total cost does not change. This mirrors the single-channel property and holds for any number of channels n. The proof in the machine-checked library of formal theorems reduces the multi-channel statement to the already-proved single-channel symmetry, J(x) = J(1/x), applied to each component.

This symmetry is one of four properties the framework proves for J_n: it is always non-negative, it is zero if and only if every channel sits at 1, it attains zero at the all-ones vector, and it is symmetric under inversion. Together these properties form a certificate, a packaged collection of theorems, that the multi-channel cost behaves like a well-behaved distance from equilibrium. The symmetry in particular means that a channel at value 2 and a channel at value 1/2 incur the same cost, a reciprocal fairness that the framework treats as a structural feature of recognition.

What Jcost_n_symm does not claim is just as important. It does not say that the multi-channel cost is symmetric under permuting channels, only under inverting each channel's value. It does not assert that J_n is the unique cost function with these properties; uniqueness is a separate question about the single-channel J, not about this additive extension. And it does not claim that the gradient flow on J_n converges to the all-ones vector, only that such descent drives x toward 1⃗, a statement about dynamics that the symmetry theorem itself does not establish.

For a reader, the practical upshot is a clear picture of how the framework handles multiple simultaneous recognitions: add the costs, and the inversion symmetry carries over channel by channel. This makes J_n a tool for comparing configurations where some channels are above equilibrium and others below, with the total cost treating both directions symmetrically. The theorem is a small but precise piece of the framework's foundation, and knowing its exact scope prevents overreading it as a claim about uniqueness, permutation symmetry, or convergence.

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

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

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

/-- 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_symm does not claim symmetry under permuting channels. It does not claim that J_n is the unique multi-channel cost function with these properties. It does not claim that gradient flow converges to the all-ones vector.

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: