Information Jcost Necessity Jcost Satisfies Information Cost

The information-cost check

An information cost is a rule that assigns a price to comparing two states. In Recognition Science, the cost of recognition, the price of registering a difference, is a number attached to the ratio between the two states. Three plain requirements define a well-behaved cost: it must be symmetric, so comparing A to B costs the same as comparing B to A; it must be zero when the states are identical, when the ratio is 1; and it must be strictly convex, meaning there is exactly one cheapest balance point and costs rise smoothly away from it. These are the axioms of the information cost structure, a formal definition in the framework's machine-checked library of formal theorems.

The declaration jcost_satisfies_information_cost proves that the canonical reciprocal cost J(x) = (x + 1/x)/2 - 1 meets all three requirements. Symmetry holds because swapping x for 1/x leaves the expression unchanged. The minimum holds because plugging in 1 gives zero. Strict convexity holds because the function curves upward on positive inputs. The proof is a theorem in the framework's library, checked by the machine, with no gaps. It shows the canonical cost is at least a legitimate information cost, not a foreign object bolted onto the theory.

In Recognition Science, this check matters because it closes a loop. The framework derives J from deeper forcing principles, but a skeptic could ask whether that derived object behaves like a cost at all. This theorem answers: yes, it satisfies the same three axioms one would demand of any information cost. The declaration does not, however, claim that these three axioms alone force J. Symmetry, minimum, and convexity admit many functions. The uniqueness story requires an extra assumption: that the cost lies in the reciprocal affine family a * (x + 1/x) + b and carries the calibration a = 1/2. Only then does the zero-at-one condition force the canonical J. That stronger claim is a separate theorem, jcost_is_unique, and this declaration does not establish it.

What the declaration does establish is a consistency result: the derived cost is not ad hoc. It satisfies the minimal structural demands of an information cost. A reader can now see that the framework's central object behaves as its role requires, at least at the level of basic axioms. The deeper question of whether those axioms uniquely select J, or whether the information-theoretic framing adds anything beyond the forcing chain, remains a separate matter.

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

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

What this page does not claim

The three axioms alone force the canonical J. The declaration proves the uniqueness theorem jcost_is_unique.

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: