Cost Jcost Logic Jcost L Zero Iff

The zero-cost point

The cost function J(x) = (x + 1/x)/2 - 1 measures the price of recognizing one object as another. It is zero only when x equals 1, meaning the object is recognized as itself. This is the statement of the theorem JcostL_zero_iff: for any positive recovered real x, the cost is zero if and only if x is 1. The recovered reals are the framework's internal number system, and the theorem transfers directly from the standard real numbers.

The cost function is symmetric: J(x) = J(1/x), so recognizing A as B costs the same as recognizing B as A. It is also nonnegative for positive x, so zero is the minimum possible cost. The function can be rewritten as (x-1)²/(2x), which makes the zero point visible: the numerator vanishes only at x = 1. This is the unique point where recognition is free, and it is the anchor for the framework's structure.

In Recognition Science, this cost is not chosen freely. The framework proves that any cost function satisfying five plain conditions (reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity) must equal this J. The composition law is the key constraint: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y). The zero-cost point is where this law and the other conditions force the unique form.

The theorem does not claim that x = 1 is the only point where the cost is defined, nor that the cost is always finite. It applies only to positive x, and the recovered-real version inherits its truth from the real-number version. The theorem also does not say what the cost means physically; it is a mathematical fact about the function, not an empirical statement about the world.

theorem JcostL_zero_iff {x : LogicReal} (hx : (0 : LogicReal) < x) :
    JcostL x = fromReal 0 ↔ x = fromReal 1 := by
  constructor
  · intro h
    rw [eq_iff_toReal_eq]
    have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
    have hx0 : toReal x ≠ 0 := ne_of_gt hx'
    have hreal : Jcost (toReal x) = 0 := by
      have := congrArg toReal h
      rwa [toReal_JcostL, toReal_fromReal] at this
    rw [Jcost_eq_sq hx0] at hreal
    have hden : (0 : ℝ) < 2 * toReal x := by nlinarith
    have hsq : (toReal x - 1) ^ 2 = 0 := by
      have := congrArg (fun y : ℝ => y * (2 * toReal x)) hreal
      field_simp [ne_of_gt hden] at this
      simpa using this
    have hsub : toReal x - 1 = 0 := sq_eq_zero_iff.mp hsq
    rw [toReal_fromReal]
    linarith
  · intro h
    rw [h, JcostL_unit0]

theorem JcostL_symm {x : LogicReal} (hx : (0 : LogicReal) < x) :
    JcostL x = JcostL x⁻¹ := by
  rw [eq_iff_toReal_eq, toReal_JcostL, toReal_JcostL, toReal_inv]
  have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
  exact Jcost_symm hx'

theorem JcostL_nonneg {x : LogicReal} (hx : (0 : LogicReal) < x) :
    (0 : LogicReal) ≤ JcostL x := by
  rw [le_iff_toReal_le, toReal_zero, toReal_JcostL]
  have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
  exact Jcost_nonneg hx'

theorem JcostL_eq_sq {x : LogicReal} (hx : toReal x ≠ 0) :
    JcostL x = (x - fromReal 1) * (x - fromReal 1) / (fromReal 2 * x) := by
  rw [eq_iff_toReal_eq]
  simp [toReal_JcostL, toReal_fromReal]
  simpa [pow_two] using Jcost_eq_sq hx

/-- Transported RCL: a recovered-real composition law becomes the existing
real composition law under `toReal`. -/
theorem compositionLawL_to_real {F : LogicReal → LogicReal}
    (hF : SatisfiesCompositionLawL F) :
    Cost.FunctionalEquation.SatisfiesCompositionLaw (transportCost F) := by
  intro x y hx hy
  unfold transportCost
  have hxL : (0 : LogicReal) < fromReal x := by
    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hx
  have hyL : (0 : LogicReal) < fromReal y := by
    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hy
  have hxy : fromReal x * fromReal y = fromReal (x * y) := by
    rw [eq_iff_toReal_eq]
    simp [toReal_fromReal]
  have hdiv : fromReal x / fromReal y = fromReal (x / y) := by
    rw [eq_iff_toReal_eq]
    simp [toReal_fromReal]
  have hL := hF (fromReal x) (fromReal y) hxL hyL
  rw [hxy, hdiv] at hL
  have h := congrArg toReal hL
  simpa [toReal_add, toReal_mul, toReal_div, toReal_fromReal] using h

What this page does not claim

The theorem does not claim that x = 1 is the only point where the cost is defined. The theorem does not claim the cost is always finite for positive x. The theorem does not claim any physical meaning for the cost function.

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/Cost/JcostLogic.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: