Cost Aczel Classification Aczel Kernel Smooth

The smoothness bridge

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, asks for functions H that satisfy H(t+u) + H(t−u) = 2H(t)H(u). Its continuous solutions are exactly the familiar trigonometric and hyperbolic functions, but proving that requires a regularity step: one must first show that continuity alone forces the solution to be infinitely differentiable, or smooth. The Hungarian mathematician János Aczél supplied this step in his classification of such equations. The Recognition Science library packages that step as a formal theorem named aczel_kernel_smooth.

In plain language, the theorem says: if H is a continuous solution of the d'Alembert equation, then H is smooth. That is the entire content. The declaration is a convenience projection, a small handle that extracts this smoothness fact from a larger structure called the AczelRegularityKernel. It does not by itself solve the equation, compute any constants, or identify which solution is the right one. It only certifies that the continuity assumption, which is easy to check in applications, upgrades to the much stronger differentiability property that later steps need.

Why does this matter for Recognition Science? The framework's central result, the uniqueness of the cost function J(x) = (x + 1/x)/2 − 1, rests on a chain of deductions. One link in that chain is the d'Alembert equation, which the cost function satisfies after a logarithmic change of variables. The smoothness bridge is what lets the framework pass from the five plain axioms of cost (reciprocal symmetry, normalization, composition, calibration, continuity) to the differential equation H'' = H, whose solutions are exponentials, and from there to the unique closed form of J. Without the bridge, the chain would stop at continuity and the uniqueness theorem would not go through.

What the declaration does not claim is equally precise. It does not assert that every continuous function satisfying the equation is smooth; that is false, and the theorem's hypothesis explicitly requires continuity. It does not derive the cost function, the golden ratio, or any physical constant; those are separate theorems that use this smoothness fact as an input. It also does not say anything about which smooth solution is selected; the equation alone admits many, and the selection comes from the other axioms. The theorem is a narrow, mechanical bridge: continuity in, smoothness out, nothing more.

For the reader, the practical consequence is that the framework's uniqueness proof does not secretly assume differentiability. The assumption is the weaker, more checkable one of continuity, and the smoothness is earned, not granted. That is the kind of provenance that lets a large claim stand on small, verified steps.

/-- Convenience projection: the smoothness theorem exported by the kernel. -/
theorem aczel_kernel_smooth [AczelSmoothnessPackage] (H : ℝ → ℝ) :
    dAlembert_continuous_implies_smooth_hypothesis H :=
  (aczelRegularityKernel H).smooth

What this page does not claim

The theorem does not claim that every continuous function satisfying the equation is smooth, only those that are already continuous. The theorem does not derive the cost function, the golden ratio, or any physical constant. The theorem does not identify which smooth solution is the correct one; that selection comes from other axioms.

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