Foundation Multi Channel Jcost Jcost N

The multi-channel cost

In ordinary mathematics, a cost function is a way of scoring how far a configuration sits from a preferred state. The multi-channel cost J_n does this for a list of n positive numbers x₁, x₂, ..., xₙ. It is defined as the sum J(x₁) + J(x₂) + ... + J(xₙ), where each J(x) = (x + 1/x)/2 − 1. Each channel contributes zero exactly when its value is 1, and contributes a positive amount otherwise. The whole sum is therefore always non-negative, and it equals zero precisely when every channel sits at 1.

This additive structure is what makes the multi-channel cost useful for tracking many independent quantities at once. It is symmetric under taking reciprocals channel by channel: swapping xᵢ with 1/xᵢ leaves the total unchanged. Gradient flow on J_n drives every channel toward 1, meaning the cost decreases as the whole configuration moves toward the all-ones point. These properties are proved in a machine-checked library of formal theorems, with no unproved assumptions in the recognition framework's own axioms. The framework models recognition events as a discrete record, and J_n is its way of scoring a multi-part record for balance.

The declaration establishes these facts and nothing more. It does not claim that any particular physical system actually minimizes J_n, nor that the all-ones point is reached in finite time. It does not assign meaning to the channels: whether xᵢ represents an amplitude, a phase, or a frequency is a modeling choice, not a theorem. The cost is a mathematical object with proved properties, and the framework's empirical claims about real systems are separate hypotheses, not consequences of this declaration.

What the declaration gives a reader is a precise vocabulary for talking about balance across many channels. If a system's state is described by n positive numbers, J_n provides a single scalar that is zero only at perfect balance and positive otherwise. That is the whole content: a definition and its proved consequences, ready to be used as a tool in larger arguments about recognition and cost.

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

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

What this page does not claim

No claim that any physical system actually minimizes J_n. No claim that the all-ones point is reached in finite time. No claim about what the channels represent; that is a modeling choice.

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: