Information Jcost Necessity

The forced cost

In mathematics, a cost function assigns a number to each possible state, measuring how expensive that state is. Recognition Science studies cost functions that describe the price of recognizing one thing as another. The framework's central object is the ledger, a discrete record of recognition events, and the cost of each event is forced by a small set of rules rather than chosen freely.

The information-cost module starts with three plain conditions. First, symmetry: recognizing x as y costs the same as recognizing y as x, so F(x) = F(1/x). Second, a minimum at balance: when x equals 1, the cost is zero, meaning the balanced state is free. Third, strict convexity: the cost curve bends upward, guaranteeing a unique stable equilibrium. These three conditions alone do not pin down a single formula; many functions satisfy them.

The theorem adds two more constraints. The cost must lie in the reciprocal affine family, meaning it has the form a * (x + 1/x) + b for some numbers a and b. And the calibration a = 1/2 is imposed. Under those conditions, the zero-at-one requirement forces the unique formula J(x) = (x + 1/x)/2 - 1. This is the canonical J-cost, and it is the only member of that family satisfying all five requirements.

The module proves both directions. The uniqueness theorem, jcost_is_unique, shows that any information cost in the reciprocal affine family with calibration a = 1/2 must equal J. The companion theorem, jcost_satisfies_information_cost, confirms that J itself meets the three base conditions: symmetry, zero minimum, and convexity. Together they establish that within this family, the canonical cost is not one option among many but the only option.

What this changes is the status of the formula. J is not an arbitrary choice made by the framework's authors; it is what the stated rules force. The module narrows the search space from all possible cost functions to exactly one, given the family and calibration. That uniqueness is what lets later results in the framework build on J with confidence.

/-- **DEFINITION: Recognition Information Cost**
    The cost function F must satisfy:
    1. Symmetric: F(x) = F(1/x) (Recognition is bi-directional).
    2. Minimum: F(1) = 0 (Balanced state has zero cost).
    3. Convexity: F is strictly convex (Unique stable equilibrium). -/
structure InformationCost (F : ℝ → ℝ) : Prop where
  symmetric : ∀ {x : ℝ}, x > 0 → F x = F (1 / x)
  minimum   : F 1 = 0
  convex    : StrictConvexOn ℝ (Set.Ioi 0) F

/-- **THEOREM: calibrated reciprocal-affine uniqueness.**
    If an information cost lies in the reciprocal affine family and carries
    the RS calibration `a = 1/2`, then the zero-at-one condition forces it
    to be the canonical J-cost on positive ratios. -/
theorem jcost_is_unique (F : ℝ → ℝ) (h : InformationCost F)
    (a b : ℝ) (h_form : ∀ x > 0, F x = a * (x + 1 / x) + b)
    (h_calibrated : a = 1 / 2) :
    ∀ x > 0, F x = Cost.Jcost x := by
  intro x hx
  have h1 : F 1 = 0 := h.minimum
  rw [h_form 1 (by norm_num)] at h1
  have hb : b = -2 * a := by linarith
  have hb_val : b = -1 := by linarith
  rw [h_form x hx, h_calibrated, hb_val]
  unfold Cost.Jcost
  field_simp [ne_of_gt hx]
  ring

/-- **Canonical J-Cost satisfies InformationCost** -/
theorem jcost_satisfies_information_cost : InformationCost Cost.Jcost := {
  symmetric := fun {x} hx => by
    simpa [one_div] using (Cost.Jcost_symm hx)
  minimum := Cost.Jcost_unit0
  convex := Cost.Jcost_strictConvexOn_pos
}

What this page does not claim

The three base conditions alone force J without the reciprocal affine family assumption. The calibration a = 1/2 is derived from deeper principles rather than imposed as a definitional choice. This module proves the full forcing chain that leads to three spatial dimensions.

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/Information/JCostNecessity.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: