Cost Aczel Theorem

The Aczél classification

The Aczél classification is a theorem of functional equations with an unreasonably strong punchline: mere continuity already implies infinite smoothness. It concerns the d'Alembert equation, the symmetry identity relating the values of a function H at t+u and t-u to its values at t and u, with H at zero normalized to one. The classification says that every continuous solution is one of exactly three functions: the constant one, a hyperbolic cosine, or a cosine. Since all three are smooth, a solution that never jumps is already infinitely differentiable.

The proof climbs a ladder. Integrating the equation produces a representation of H as a quotient of differences of an antiderivative. Each pass through the representation buys one more degree of differentiability: continuous becomes differentiable once, then twice, and so on through every finite order. Once H is smooth, differentiating the identity twice yields the ordinary differential equation H'' = c·H, with c the second derivative of H at zero. That equation has exactly the three named families as solutions, which closes the classification.

Until this proof, the framework's foundations carried the classification as their one remaining hypothesis; the derivations that force the golden ratio, the eight-tick cycle, and three spatial dimensions all stood on it. The smoothness that the framework previously assumed as its final hypothesis is now established unconditionally, with no sorry placeholders and no axioms of its own. What the theorem supplies is regularity, the smoothness the rest of the framework had been borrowing; it is a mathematical fact about an equation, not a physical claim about the world.

THEOREM dAlembert_contDiff_top · IndisputableMonolith/Cost/AczelTheorem.lean

THEOREM dAlembert_contDiff_nat · IndisputableMonolith/Cost/AczelTheorem.lean

THEOREM dAlembert_to_ODE_general · IndisputableMonolith/Cost/AczelTheorem.lean

THEOREM h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean

What this page does not claim

The Aczél classification is not a physical law and makes no empirical prediction. The scale parameter λ inside the cosine and hyperbolic-cosine forms is not fixed by the theorem. The uniqueness of the cost function is not restated here; this page covers the smoothness step.

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