Information Jcost Necessity Jcost Is Unique

The uniqueness claim

The cost function J(x) = (x + 1/x)/2 - 1 measures the price of recognizing a ratio x. It assigns zero cost to the balanced state x = 1, treats reciprocal ratios symmetrically so that x and 1/x cost the same, and rises smoothly as x moves away from 1. These three properties, symmetry, a minimum at 1, and strict convexity, define what the framework calls an information cost: a discrete record of how expensive it is for a system to register a ratio.

The theorem jcost_is_unique asks a sharper question. Suppose a cost function F has those three properties and also belongs to a specific family: F(x) = a(x + 1/x) + b, a linear combination of the reciprocal and its inverse. Within that family, the theorem proves that the calibration a = 1/2 and the zero-at-one condition together force F to equal J exactly. No other member of the reciprocal affine family satisfies all the requirements. The proof is machine-checked in the framework's library of formal theorems, and the canonical J itself is verified to satisfy the information cost conditions.

The theorem does not claim uniqueness across all possible cost functions. Symmetry, minimum, and convexity alone permit many functions; the result only pins down J within the reciprocal affine family. It also does not derive the calibration a = 1/2 from first principles. That value enters as a premise, a definitional choice about scaling, not as a conclusion. What the theorem establishes is conditional: if a cost lies in this family and carries this calibration, then it must be J.

In Recognition Science, this conditional uniqueness supports a larger forcing chain. The framework models recognition costs as forced rather than chosen, and J's special position within its family is one link in that argument. But the theorem itself stays narrow. It settles a question about one family of functions, and it leaves the broader question of why recognition should take this particular form to the framework's other results.

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

Uniqueness across all cost functions, since symmetry, minimum, and convexity alone do not force J. A derivation of the calibration a = 1/2, which enters as a premise rather than a conclusion. Any claim about why recognition costs should take this form, which belongs to the broader forcing chain.

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: