Composition Law

The forced composition law

A composition law is a rule that combines two quantities into a third. In cost problems, it says how the cost of doing two operations together is determined by the costs of doing them separately. When the operations are compared through ratios, the rule takes the form F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y) for positive x and y. This is a functional equation: the unknown is the whole function F, not a single number. A distinguished solution is F(x)=(x+1/x)/2-1, which is cosh(ln x)-1. The function is zero at x=1, symmetric when x is replaced by 1/x, and never negative, because the average of x and 1/x is always at least 1. Write x=e^a and y=e^b; then the equation says that the cost depends on the sum a+b and the difference a-b in a way that mirrors how multiplying and dividing the original ratios combine. It grows as x moves away from 1 in either direction.

The equation is a close relative of the d'Alembert equation, H(t+u)+H(t-u)=2H(t)H(u), studied by Jean le Rond d'Alembert in the 1700s. Cosine and hyperbolic cosine both satisfy it, which is why the two solution families appear. In logarithmic coordinates, the composition law is equivalent to the cosh-addition identity underlying d'Alembert's equation. The classical regularity theory for this equation, developed in the mid-20th century by János Aczél and his school, says that continuity upgrades to smoothness, so the second derivative at zero is meaningful. Over the reals, the equation alone leaves room for the family H(t)=cosh(k t) and the family H(t)=cos(k t). The calibration H''(0)=1 is exactly what picks k=1 in the first family and rules out the second. The uniqueness result therefore depends on the calibration condition as much as on the equation itself.

In Recognition Science, the same equation is the forced composition law for what the framework calls recognition costs. Here recognition is an act of identifying a thing as a case of a pattern, and a cost is the number a ledger, a discrete record of such acts, assigns to that act. The framework defines a recognition cost as a function F on positive numbers that is reciprocal, normalized at 1, calibrated (a second-derivative condition fixes the scale of the cost near 1), and continuous. The composition law is the fifth condition. A machine-checked library of formal theorems derives that any F satisfying all five must equal J(x)=(x+1/x)/2-1. The same library checks that J itself satisfies the cosh-addition identity, and therefore the composition law, so the forced function is a genuine solution rather than an empty equation. The composition law matters because it is the condition that closes the gap: with the other four conditions and the composition law, the family of possible costs collapses to one function.

MODEL SatisfiesCompositionLaw · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM Jcost_cosh_add_identity · composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

What this page does not claim

The composition law alone does not force J; the other four conditions are required. Not every continuous solution of the d'Alembert equation is cosh; without calibration the cosine and scaled cosh families also satisfy the equation. The composition law is a defining condition inside the framework, not an independently measured property of any physical system.

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: