Cost Jcost Logic

The cost of recognition

The cost of recognition is the price reality pays, in this framework, for telling two things apart. The framework, Recognition Science, starts from a discrete record of events, a ledger. Each entry is a recognition event: a comparison, a distinction, a match. The central question is what such comparisons must cost. The answer, proved in a machine-checked library of formal theorems, is a single formula: J(x) = (x + 1/x)/2 - 1. The variable x is the ratio of the two things being compared. When the ratio is 1, the things are identical, and the cost is 0. When the ratio is 2, the cost is 0.25; when it is 3, the cost is 0.666...; when it is 10, the cost is 4.95.

The formula is not chosen. It is forced. Any cost function that satisfies five plain conditions must equal this J. The conditions are: symmetry (comparing x to y costs the same as comparing y to x), zero cost at equality, a composition law (the cost of doing two comparisons in sequence is determined by the costs of the parts), a calibration condition, and continuity. The composition law has a concrete form: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y). This is the equation that pins the solution down. Without continuity, other solutions exist; with it, only J survives. The proof is a theorem in the framework's library, and it uses no special axioms beyond the standard logical ones.

The function has a classical cousin. The expression (x + 1/x)/2 is the arithmetic mean of a number and its reciprocal. Subtracting 1 shifts the zero to x = 1. The formula is symmetric under swapping x and 1/x, which matches the symmetry of comparison. It is always nonnegative for positive x, and it is zero only at x = 1. These properties are not assumed; they are proved from the definition. The library also proves an equivalent squared form: J(x) = (x - 1)^2 / (2x), which makes the nonnegativity visible at a glance.

In Recognition Science, this cost is the foundation. From J, the framework derives the golden ratio as the unique self-similar scaling, an eight-tick recognition cycle, the number 2^3, and three spatial dimensions. The cost formula is the first rung. It is also the entry point for the framework's logical machinery: the same theorems are proved both for ordinary real numbers and for a recovered-real type that the framework uses internally. The two versions agree, and the library proves that agreement explicitly.

What this means in practice: if you accept the five conditions, you get the cost function for free. You do not get to pick a cheaper or more expensive one. The framework's claim is that recognition, wherever it happens, is priced by this formula. That is a large claim, and the page does not prove it here; it only reports what the framework's own library establishes.

/-- Canonical reciprocal cost on recovered reals. -/
def JcostL (x : LogicReal) : LogicReal :=
  (x + x⁻¹) / fromReal 2 - fromReal 1

/-- Canonical reciprocal cost on recovered reals. -/
def JcostL (x : LogicReal) : LogicReal :=
  (x + x⁻¹) / fromReal 2 - fromReal 1

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

/-- Recognition Composition Law on recovered reals for a cost function. -/
def SatisfiesCompositionLawL (F : LogicReal → LogicReal) : Prop :=
  ∀ x y : LogicReal, (0 : LogicReal) < x → (0 : LogicReal) < y →
    F (x * y) + F (x / y)
      = fromReal 2 * F x * F y + fromReal 2 * F x + fromReal 2 * F y

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_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]

What this page does not claim

This page does not claim that the five conditions are physically necessary, only that they force J if accepted. This page does not claim that the framework's derivation of the golden ratio or three dimensions is proved here. This page does not claim that the cost function applies outside the framework's ledger model.

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: