Cost Aczel Classification H D Alembert Of Composition

The d'Alembert bridge

In 1747, Jean le Rond d'Alembert studied vibrating strings and wrote down a functional equation that bears his name. For a function H of a real variable, the equation reads H(t+u) + H(t-u) = 2 H(t) H(u). Its solutions include the familiar hyperbolic cosine, H(t) = cosh(kt), and the ordinary cosine, H(t) = cos(kt), among others. The equation encodes a kind of symmetry: the value at a sum and difference of two points is determined by the product of the values at those points.

What makes the d'Alembert equation powerful is a classification result proved by János Aczél and others in the mid-twentieth century. Without any regularity assumption, the equation admits wild, pathological solutions. But if the solution is continuous, even only at a single point, it must be smooth, and it must satisfy the ordinary differential equation H'' = H. This is the Aczél regularity kernel: continuity collapses the zoo of exotic solutions down to a one-parameter family of well-behaved exponentials and trigonometric functions.

In Recognition Science, the framework models a cost, a real number measuring the effort of recognizing one object as another, as a function F on positive reals. The framework's library, a machine-checked collection of formal theorems, proves that any cost satisfying its five primitive assumptions also satisfies the d'Alembert equation after a logarithmic change of variables. The declaration H_dAlembert_of_composition establishes exactly this bridge: it derives the d'Alembert equation for H(t) = F(e^t) + 1 from the composition law alone, before any continuity or calibration assumptions are invoked.

The composition law itself is the requirement that the cost of recognizing x as z is the sum of the costs of recognizing x as y and y as z, for an intermediate y. This law forces the d'Alembert structure. The theorem does not claim that the composition law alone determines the cost function. It does not claim that every solution of the d'Alembert equation is a valid cost. The full uniqueness result, that F(x) = (x + 1/x)/2 - 1, requires the additional hypotheses of normalization, calibration, and continuity, which together supply the Aczél kernel that selects the smooth solution.

What the declaration changes is the architecture of the proof. Instead of routing through a separate Jensen sketch, the public theorem primitive_to_uniqueness_aczel takes the primitive cost hypotheses directly and uses the Aczél kernel as the sole regularity bridge. The d'Alembert equation is the seam where a discrete ledger of recognition events becomes a smooth curve, and the classification theorem guarantees that no other continuous curve can satisfy the same constraints.

private theorem H_dAlembert_of_composition (F : ℝ → ℝ)
    (hComp : SatisfiesCompositionLaw F) :
    ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u := by
  let Gf : ℝ → ℝ := G F
  have h_direct : DirectCoshAdd Gf :=
    CoshAddIdentity_implies_DirectCoshAdd F ((composition_law_equiv_coshAdd F).mp hComp)
  intro t u
  have hG := h_direct t u
  have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
    calc
      (Gf (t + u) + 1) + (Gf (t - u) + 1)
          = (Gf (t + u) + Gf (t - u)) + 2 := by ring
      _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by
            simpa [Gf] using hG
      _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
  simpa [Gf, H, G] using h_goal

/-- Official public T5 theorem with an explicit Aczél kernel seam.

The public statement now takes the primitive cost hypotheses directly and uses
`AczelRegularityKernel` as the sole regularity bridge. This makes the T5 seam
explicit without routing through `JensenSketch`. -/
theorem primitive_to_uniqueness_of_kernel (F : ℝ → ℝ)
    (hF : PrimitiveCostHypotheses F)
    (hKernel : AczelRegularityKernel (H F)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  have h_H0 : H F 0 = 1 := H_one_of_normalized F hF.normalized
  have h_H_cont : Continuous (H F) :=
    H_continuous_of_positive_continuous F hF.continuous
  have h_H_dAlembert : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u :=
    H_dAlembert_of_composition F hF.composition
  have h_smooth : ContDiff ℝ ⊤ (H F) :=
    hKernel.smooth h_H0 h_H_cont h_H_dAlembert
  exact law_of_logic_forces_jcost_with_regularization F
    hF.reciprocal hF.normalized hF.composition hF.calibrated hF.continuous
    hKernel.smooth hKernel.ode
    (ode_regularity_continuous_of_smooth h_smooth)
    (ode_regularity_differentiable_of_smooth h_smooth)
    (ode_regularity_bootstrap_of_smooth h_smooth)

/-- 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 composition law alone does not force the cost function to be J(x). The d'Alembert equation does not by itself select the smooth solution without the Aczél kernel. The theorem does not prove that every continuous solution of the d'Alembert equation is a valid recognition cost.

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: