Cost Functional Equation

The Cost Functional Equation

The cost functional equation is the central object of Recognition Science. It is the equation that any recognition cost function, the price reality pays to register a match, must satisfy. The framework proves that only one formula fits: J(x) = (x + 1/x)/2 - 1. This is not a choice or a fit; it is forced by five plain conditions, and the forcing is a established theorem in Lean 4.

The five conditions are reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. Reciprocal symmetry says the cost of recognizing a ratio is the same as recognizing its reciprocal. Zero cost at unity says recognizing a perfect match costs nothing. The composition law forces how costs combine when ratios multiply and divide. Calibration sets the local scale of the cost near unity. Continuity rules out jumps. The theorem law_of_logic_forces_jcost in the module IndisputableMonolith/Cost/FunctionalEquation.lean proves that any function meeting all five conditions must equal J(x) on the positive reals.

The proof works by a change of coordinates. Writing the cost in log coordinates turns the composition law into a d'Alembert functional equation, the same equation that characterizes hyperbolic cosine. The theorem dAlembert_cosh_solution shows that a continuous solution with the right local scale must be cosh. Translating back, the cost function becomes cosh(log x) - 1, which simplifies to (x + 1/x)/2 - 1. The module also proves that the composition law alone is equivalent to the cosh addition identity, and that the log-curvature condition forces normalization.

What the module establishes in plain language is this: the cost of recognition is not a free parameter. If reality keeps a ledger of recognition events at all, and if the cost obeys five plain rules, then the formula is fixed. From this single formula, the framework derives the golden ratio, an eight-tick recognition cycle, and three spatial dimensions. The cost functional equation is the first link in that chain.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_cosh_solution · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM logCurvature_forces_normalized · IndisputableMonolith/Cost/FunctionalEquation.lean

What this page does not claim

This answer does not claim that the cost functional equation is derived from physical measurements. This answer does not claim that the five conditions are themselves established rather than assumed. This answer does not claim that the cost functional equation alone yields the golden ratio or spatial dimensions without further theorems.

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: