Cost Aczel Classification Primitive To Uniqueness Of Kernel

The uniqueness bridge

The d'Alembert equation, written H(t+u) + H(t−u) = 2H(t)H(u), is a classical functional equation studied since Jean le Rond d'Alembert's 1747 work on vibrating strings. Its continuous solutions are well understood: they are exactly the hyperbolic cosine, the ordinary cosine, and the constant functions. The equation appears whenever a quantity splits into independent parts, so it shows up across physics and probability. The Recognition Science framework uses this classical result as a bridge, not as an end in itself.

In Recognition Science, a cost is a number that measures how expensive it is for reality to recognize one thing as another, with zero cost meaning perfect agreement. The framework's library, a machine-checked collection of formal theorems, proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 − 1. The conditions are reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. The theorem named primitive_to_uniqueness_of_kernel states this result directly: given those five hypotheses, the cost function F at any positive x equals Jcost x.

The proof works by changing variables. Writing H(t) = F(e^t) + 1 transforms the five cost conditions into the d'Alembert equation plus a smoothness condition. A classical theorem of János Aczél says that continuous d'Alembert solutions are smooth, and once smoothness is available, a standard argument reduces the equation to the ordinary differential equation H'' = H. Solving that ODE gives H(t) = cosh(t), which translates back to the unique cost function J. The framework packages this two-step argument as a single regularity kernel, a named structure that records both the smoothness result and the ODE step.

The theorem does not claim that the five conditions are necessary, only sufficient. It does not prove that the cost function is unique among all functions, only among those satisfying the hypotheses. It also does not claim that the d'Alembert equation itself forces the result; the continuity condition is essential, and without it pathological solutions exist. The framework's contribution is to show that its five natural-looking conditions, each with a clear physical interpretation, happen to select exactly the nice solution.

What the theorem changes is the status of the cost function. Before this result, J was a plausible guess. After it, within the framework, J is forced: any cost function meeting the five conditions must be J, and the proof is checked by machine. This turns a definitional choice into a derived theorem, and it is the first step in a chain that leads to the golden ratio, an eight-tick cycle, and three spatial dimensions. The classical d'Alembert equation, studied for centuries, turns out to be the hidden engine behind the framework's most distinctive claims.

/-- 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 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

What this page does not claim

The five conditions are necessary for J to be the cost function, only sufficient. The d'Alembert equation alone forces the result; the continuity condition is essential. The theorem applies to cost functions that fail any of the five hypotheses.

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: