Two Premises Reciprocal Cost

Two premises, one cost

Imagine you are keeping books for the universe. Every time one thing recognizes another, you must write down a number, the cost of that recognition event. The question is not what number you choose, but what number you are forced to write. The answer, proved in Lean 4 with no special axioms, is that two conditions alone pin the cost function to J(x) = (x + 1/x)/2 - 1. The first condition is a symmetry: recognizing x and recognizing its reciprocal 1/x must cost the same, because the ledger cannot tell which direction the recognition ran. The second is a composition law: the cost of a product x*y and the cost of a ratio x/y must combine in a fixed way, mirroring how the recognition events themselves combine. That is all.

The proof is not a long march through analysis. In logarithmic coordinates, where multiplication becomes addition, the composition law becomes d'Alembert's functional equation, a classical object. The symmetry condition makes the solution even. A single calibration condition, fixing the second-order behaviour at the identity to be exactly 1, then does two jobs at once: it rules out the constant solution and it forces the solution to be the hyperbolic cosine. The descent from there is elementary. The doubling relation H(2s) = 2H(s)^2 - 1, which is the Chebyshev polynomial in disguise, lets you transport the value at one small point outward to every dyadic scale, exactly. The calibration opens a window near the origin where the solution must stay above 1, which is precisely where the inverse hyperbolic cosine is defined, and iteration does the rest. The classical route through Aczél's classification of continuous solutions is available, but the Lean proof does not need it; the descent is about two hundred lines and uses no ODE theory.

What the two premises leave open is not a gap in the proof but a choice in the framework. The calibration condition, the number 1 that fixes the scale, is a single point of input. It is not derived from anything deeper; it is the one free parameter in the whole construction. The theorem proves that if you accept the symmetry and the composition law, and you calibrate the second-order behaviour to 1, then the cost function is forced. It does not prove that the calibration must be 1. That is a definitional choice, a model, not a theorem. The distinction matters because the entire edifice of Recognition Science, from the golden ratio to three spatial dimensions, rests on this cost function. The proof shows the edifice is stable under its two structural premises, but the calibration is the keystone that is placed by hand.

The consequence is that the reciprocal cost is not one option among many. It is the unique function satisfying the symmetry and the composition law with the given calibration, and the proof is machine-checked. What remains open is the question of where the calibration itself comes from, whether it can be derived from a deeper principle or must remain an input. That is a target for future work, not a failure of the theorem. The theorem's strength is that it isolates exactly what is assumed and exactly what is forced, and the forced part is everything that matters for the structure that follows.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM hasLogCurvature_full_filter_forces_zero · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM hasLogCurvature_full_filter_forces_zero · IndisputableMonolith/Cost/FunctionalEquation.lean

MODEL HasLogCurvature · IndisputableMonolith/Cost/FunctionalEquation.lean

What this page does not claim

The calibration value of 1 is not derived; it is an input. The proof does not show that the composition law is the only possible way for recognition events to combine. The theorem does not address where the cost function applies in physical reality.

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: