Cost Aczel Classification Primitive To Uniqueness Aczel

The uniqueness theorem

The d'Alembert equation, written H(t+u) + H(t-u) = 2H(t)H(u), is one of the oldest functional equations in analysis. It asks for functions whose value at a sum and difference combine like the cosine addition formula. In 1747, Jean le Rond d'Alembert derived it while studying vibrating strings, and it has since appeared wherever symmetry constrains a process. The classical theorem, due to János Aczél in the twentieth century, classifies its continuous solutions: they are exactly the hyperbolic cosine and its relatives, with no exotic alternatives once continuity is assumed.

Recognition Science uses this classical result as a bridge. The framework's starting point is a ledger, a discrete record of recognition events, and a cost, the forced price of recording one event. The cost function F(x) measures the price of recognizing a change of size x. The framework assumes five plain conditions: reciprocal symmetry F(x) = F(1/x), zero cost at unity F(1) = 0, a composition law linking costs at products, a calibration condition, and continuity on positive inputs. These are the primitive hypotheses, stated directly without intermediate sketches.

The theorem primitive_to_uniqueness_aczel in the framework's machine-checked library of formal theorems proves that these five conditions leave no room for choice. It first shows that the composition law, after a logarithmic change of variables, becomes the d'Alembert equation. Continuity then triggers the Aczél classification: the only continuous solutions are smooth, and the smooth solutions satisfy the ordinary differential equation H'' = H. Solving that equation forces the cost to be exactly J(x) = (x + 1/x)/2 - 1 for every positive x. The proof is fully formalized, with no gaps and no framework-specific axioms, only the standard logical postulates of the ambient type theory.

The result is a uniqueness theorem, not a derivation of the cost from nothing. It shows that if a cost function satisfies the five stated conditions, then it must be J. It does not claim that any actual physical process must satisfy those conditions; that is a separate modeling question. The theorem also does not identify the constant 44π or any other seed value, and it says nothing about the fine-structure constant. Its scope is strictly conditional: given the hypotheses, the conclusion follows with mathematical certainty.

What the theorem changes is the shape of the framework's foundation. Instead of assuming the cost formula as a postulate, the framework derives it from five simpler, individually plausible conditions. The Aczél classification supplies the regularity that turns a functional equation into a differential equation, and the differential equation has a unique solution. A reader who accepts the five conditions must accept J; there is no other continuous option.

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

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

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

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

What this page does not claim

The theorem does not claim that any actual physical process must satisfy the five conditions. It does not identify the constant 44π or derive the fine-structure constant. It does not assert the cost formula as an axiom; it derives it from the 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: