Cost Aczel Classification

The regularity bridge

The Aczel classification theorem is a classical result in functional equations. It concerns the d'Alembert equation, written here as H(t+u) + H(t-u) = 2H(t)H(u), and it answers a regularity question: if a solution is merely continuous, must it be smooth? The classical answer is yes. The theorem, due to Jean d'Alembert's 1747 work on vibrating strings and later sharpened by János Aczél, shows that continuity alone forces infinite differentiability for this equation. This is the bridge that lets a weak, qualitative assumption (continuity) yield a strong, quantitative conclusion (a second-order differential equation).

The classical solution family is worth stating precisely. Without any regularity assumption, the d'Alembert equation admits pathological, discontinuous solutions built from Hamel bases. The continuity assumption selects the nice family: H(t) = cosh(kt) for a real constant k. The Aczel classification theorem is what rules out the pathological branch and leaves only the smooth one. This is the standard regularity story that any treatment of the equation must tell, and it is the story the Recognition Science framework imports.

In Recognition Science, the framework models a ledger, a discrete record of recognition events, and defines the cost of a recognition as a function F(x) on positive ratios. The framework's central theorem states that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The five conditions are reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. The composition law, written in full as F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y), is what connects the cost function to the d'Alembert equation after a logarithmic change of variables.

The framework's formal library packages the Aczel theorem as the regularity bridge in this forcing chain. Its machine-checked results establish two facts. First, a continuous d'Alembert solution is smooth. Second, once smoothness is available, the calibrated ODE kernel H'' = H follows. These two facts are packaged into a structure called AczelRegularityKernel, and the library shows that any cost function satisfying the five primitive hypotheses, together with this kernel, must equal Jcost. The result primitive_to_uniqueness_aczel states this uniqueness directly: under the five assumptions, F x = Jcost x for every positive x.

The practical consequence is that the downstream uniqueness proof no longer needs to touch the raw Aczel axiom. The classification step is isolated as a seam, and the rest of the forcing chain can rely on the ODE kernel it produces. This is what the framework establishes in plain language: the Aczel theorem supplies the one missing regularity step, and with it, the five plain assumptions force a single, explicit cost function. The framework's library proves this chain with no framework-specific axioms, only the standard three axioms of the ambient type theory.

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

/-- Convenience projection: the ODE kernel exported by the classification step. -/
theorem aczel_kernel_ode [AczelSmoothnessPackage] (H : ℝ → ℝ) :
    dAlembert_to_ODE_hypothesis H :=
  (aczelRegularityKernel H).ode

/-- Convenience form of the canonical T5 theorem using the current Aczél
smoothness package to supply the regularity kernel automatically. -/
theorem primitive_to_uniqueness_aczel [AczelSmoothnessPackage] (F : ℝ → ℝ)
    (hF : PrimitiveCostHypotheses F) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  primitive_to_uniqueness_of_kernel F hF (aczelRegularityKernel (H F))

What this page does not claim

The Aczel classification theorem itself is not proved in the framework; it is imported as a package. The framework does not derive the five primitive cost hypotheses; they are assumptions. The uniqueness result does not hold without the AczelRegularityKernel regularity bridge.

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: