Cost Aczel Classification Primitive Cost Hypotheses

Primitive cost hypotheses

In the Recognition Science account, a ledger is a discrete record of events, and the cost of a recognition event is the price the ledger pays to record it. The declaration PrimitiveCostHypotheses collects the five plain conditions that any such cost function must satisfy: it treats a value and its reciprocal symmetrically, charges zero when the value is one, obeys a forced composition law, meets a calibration condition, and is continuous on positive inputs.

The classical mathematics here is the d'Alembert functional equation, which dates to Jean le Rond d'Alembert's 1747 work on vibrating strings. The framework's library, a machine-checked collection of formal theorems, proves that these five primitive conditions are enough: any function F satisfying them must equal J(x) = (x + 1/x)/2 - 1 for every positive x. The proof proceeds by changing variables to turn the composition law into the d'Alembert equation, then using a regularity result to pass from continuous solutions to smooth ones, and finally deriving the second-order differential equation H'' = H that pins down the unique solution.

The regularity step matters because the d'Alembert equation alone admits pathological solutions. Without the continuity hypothesis, functions built from Hamel bases also satisfy the equation. The Aczel classification theorem, named for János Aczél, supplies the bridge: it shows that continuous d'Alembert solutions are smooth, which is what lets the framework derive the differential equation. The declaration bundles this bridge as a separate kernel, so the downstream uniqueness theorem depends on the classification seam rather than on the raw Aczél axiom directly.

In Recognition Science, this result is the T5 milestone in the forcing chain. It derives the uniqueness of the cost function from the five primitive hypotheses, and the golden ratio phi emerges later as the unique self-similar scaling of that cost. The declaration itself does not prove that any actual physical process satisfies these hypotheses; it only states what follows if they do.

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

/-- Canonical public T5 input bundle.

This is the primitive-to-uniqueness route exposed to the rest of the public RS
surface. `JensenSketch` remains available as a compatibility layer, but the
official statement now records the reciprocal-cost, normalization, composition,
calibration, and continuity assumptions explicitly. -/
structure PrimitiveCostHypotheses (F : ℝ → ℝ) : Prop where
  reciprocal : IsReciprocalCost F
  normalized : IsNormalized F
  composition : SatisfiesCompositionLaw F
  calibrated : IsCalibrated F
  continuous : ContinuousOn F (Set.Ioi 0)

/-- 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 declaration does not prove that any physical process actually satisfies the five hypotheses. The continuity hypothesis is essential; without it, the d'Alembert equation admits pathological Hamel-basis solutions. This result does not derive the golden ratio; it only sets the stage for that later step.

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: