Reciprocal Cost

Definition

Reciprocal cost is a function F on positive reals that prices mismatch under two structural demands. First, F(x) equals F(1/x): the price of a ratio does not depend on which side is treated as the base. Second, products and quotients combine under a single composition identity. Under those demands, and after one local scale fix at the identity, the only continuous solution is J(x) = (x + 1/x)/2 − 1. That formula is not a decorative choice. It is the object every later ratio in the theory inherits.

In log coordinates the composition identity becomes d'Alembert's functional equation, a classical equation whose even continuous solutions are hyperbolic cosine (up to the scale fix). The reciprocal symmetry is what makes the solution even. The scale fix, written as unit log-curvature at the origin, kills the constant branch and selects cosh. Translating back to the original variable recovers J. The chain that carries this selection is machine-checked under a regularity package; the public anchor is the forcing theorem that concludes F equals J on the positive reals.

What this does not settle is the origin of the scale fix itself. The number that sets curvature to 1 is an input, not a derived constant. Everything downstream that uses J inherits that input. The definition of reciprocal cost therefore has a sharp split: the shape of the function is forced, and the scale that names which cosh solution is chosen remains a model choice until a deeper derivation closes it.

THEOREM IsReciprocalCost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

MODEL HasLogCurvature · IndisputableMonolith/Cost/FunctionalEquation.lean

What this page does not claim

That the calibration value 1 is forced by reciprocity and composition alone. That every possible combining rule for recognition events is ruled out. That the page names a physical experiment that measures J directly.

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: