Cost Jcost Logic Jcost L Eq Sq

The cost in closed form

The cost function J(x) = (x + 1/x)/2 - 1 measures the price of recognizing one thing as another. For any positive number x, it returns a nonnegative value that is zero exactly when x equals 1, meaning no cost when the thing matches itself. The declaration JcostL_eq_sq rewrites this definition into a single closed form: Jcost(x) equals (x - 1)^2 / (2x). This is not a new assumption; it is the same function expressed differently, and the equality holds for every nonzero x.

The closed form makes the behavior of the cost visible at a glance. Because the numerator is a square, the cost can never be negative, and it reaches zero only at x = 1. As x moves away from 1 in either direction, the cost grows, slowly at first and then without bound. The formula also exposes the symmetry J(x) = J(1/x): swapping the two things being compared leaves the cost unchanged, since (x - 1)^2 / (2x) equals (1/x - 1)^2 / (2/x). This reciprocal symmetry is one of the five plain conditions from which the whole cost function is derived.

In Recognition Science, the ledger, a discrete record of recognition events, is the starting point, and this cost is what the ledger must pay. The framework proves that any cost function satisfying the five conditions must equal this J, not merely approximate it. The closed form is the practical face of that theorem: it lets anyone compute the cost for any ratio without solving equations. The declaration itself is a theorem in the framework's machine-checked library of formal theorems, and it is tagged as proved, meaning it follows from the definition with no extra assumptions.

What the declaration does not claim is just as important. It does not say why this particular cost is the right one; that is the job of the uniqueness theorem, which requires the five conditions. It does not assert that any real process actually pays this cost; the framework models recognition, and the model's fit to physics is a separate empirical question. It also does not claim anything about the fine-structure constant, the Riemann Hypothesis, or any other specific physical or mathematical result. The declaration is a piece of algebra: a definition and its equivalent form, nothing more.

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

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'

What this page does not claim

The declaration does not prove that the cost function is unique; that requires the five conditions as premises. The declaration does not state that any physical process actually incurs this cost; it is a definitional identity within the framework. The declaration says nothing about the fine-structure constant or the Riemann Hypothesis.

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: