Information Jcost Necessity Information Cost

The information-cost postulate

In mathematics, a cost function assigns a number to each possible state, measuring how far that state sits from a preferred one. The Recognition Science framework's ledger, a discrete record of recognition events, needs such a function to price the distance between any two observations. The declaration InformationCost lays down three plain conditions any such pricing must meet. First, symmetry: recognizing x from y costs the same as recognizing y from x, so F(x) = F(1/x) for positive ratios. Second, a minimum at balance: when the two sides are equal, the cost is zero, F(1) = 0. Third, strict convexity: the cost curve bends upward everywhere on the positive reals, which guarantees a unique stable equilibrium rather than a flat valley of equally cheap states.

These three conditions by themselves do not single out any one formula. An infinite family of functions satisfies them, including simple powers and logarithmic variants. The framework's library, a machine-checked collection of formal theorems, proves uniqueness only after adding two more restrictions. The cost must lie in the reciprocal affine family, meaning it has the form a·(x + 1/x) + b for constants a and b. And the calibration a = 1/2 must hold. With those two extra premises, the theorem jcost_is_unique forces the canonical form J(x) = (x + 1/x)/2 − 1 on every positive ratio. The library also verifies the converse: this J itself satisfies all three original conditions, so the characterization is exact.

What the declaration does not claim matters as much as what it proves. It does not derive the calibration a = 1/2 from the three conditions; that value is an additional postulate, not a consequence. It does not prove that every conceivable cost function must be J, only that within the reciprocal affine family with unit calibration, J is the unique option. And it does not establish that recognition costs in the physical world actually obey these axioms. The declaration defines a class of functions and proves a uniqueness theorem inside that class; whether reality picks this class is a separate empirical question the framework addresses elsewhere.

The practical upshot is a sharp boundary. A reader who sees the three conditions alone might think they force J; the library shows they do not. A reader who sees the full theorem might think it applies to all costs; it applies only to the calibrated affine family. The declaration earns its place by making the precise logical geography visible: which premises are load-bearing, which are choices, and which remain open.

/-- **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 calibration a = 1/2 is derived from the three conditions; it is an additional postulate. Every conceivable cost function is forced to be J; only the reciprocal affine family with unit calibration is covered. Physical recognition events in the world are proven to obey these axioms; the declaration defines a class and proves uniqueness inside it.

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: