Jcost

The price of a ratio

Every positive number can be read as a ratio between two amounts. The expression J(x) = (x + 1/x)/2 - 1 turns that ratio into a price: zero when x = 1, positive for every other x, and unchanged when x is replaced by 1/x. The same price, 0.25, applies to 2 and to 1/2. Near x = 1 the price is approximately (x - 1)^2/2, so a small mismatch is paid quadratically, while for large x the price grows like x/2.

The substitution x = e^t brings out an underlying symmetry: J(e^t) = cosh t - 1, where hyperbolic cosine cosh t = (e^t + e^{-t})/2. Adding 1 turns that identity into the classical d'Alembert functional equation: H(t+u) + H(t-u) = 2H(t)H(u) with H(t) = cosh t. The equation carries d'Alembert's name from 18th-century analysis. Continuity, H(0) = 1, the d'Alembert equation, and a second derivative of 1 at 0 force H(t) = cosh t.

In Recognition Science, this function is called the recognition cost function. A ledger is a discrete record of events; a recognition is an event in which the ledger registers a ratio x between two amounts, and the cost of registering that ratio is what J charges. The framework's central theorem states that J is the only possible cost function of this kind. Any function on positive reals that is reciprocal-symmetric, normalized to zero at 1, obeys the composition law, is calibrated, and is continuous must be J. The composition law links the cost of xy and x/y to the costs of x and y; calibration fixes the second derivative at 1 to 1. The proof is checked in the framework's library, a collection of formal theorems verified by the the formal library 4 proof assistant.

One concrete value anchors the function in the framework's mathematics: at the golden ratio phi = (1 + sqrt 5)/2, J(phi) = phi - 3/2, a positive number. The useful consequence is the uniqueness theorem itself. Any proposed cost function can be settled by checking the five conditions; if they all hold, the formula is decided.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_cosh_solution_aczel · IndisputableMonolith/Cost/FunctionalEquation.lean

What this page does not claim

No claim that the five conditions are themselves derived rather than assumed as the framework's axioms. No claim that a smaller set of conditions, for instance reciprocal symmetry alone, forces J. No claim that the uniqueness theorem identifies any physical process as a recognition event; the physical bridge is open.

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/FunctionalEquation.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: