IndisputableMonolith.Cost.AczelClassification
The AczelClassification module extracts and re-exports the theorem-level payload of Aczel's classification for continuous solutions to the d'Alembert functional equation, tailored for cost theory in Recognition Science. It imports the smoothness result establishing C^∞ regularity via integration bootstrap and the explicit classification into the constant solution or cosh forms. Researchers deriving T5 J-uniqueness or dimensional constraints cite this module to access analytic cost kernels without the full proof machinery. The module structure,
claimEvery continuous solution $H:ℝ→ℝ$ of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^∞$ and equals either the constant function 1 or $H(t)=cosh(λt)$ for some constant $λ$.
background
This module resides in the Cost domain and supplies the Aczel classification seam for T5 cost uniqueness. It draws on the functional equation helpers that support the J-cost kernel, where continuous solutions to the d'Alembert relation appear as normalized cost functions. The imported AczelTheorem states the full classification (constant or hyperbolic cosine) while AczelProof establishes analyticity from continuity alone via antiderivative representation.
proof idea
This is a definition and extraction module with no internal proofs. It imports AczelTheorem to expose the classification statement, AczelProof to expose the integration bootstrap that upgrades continuity to C^∞, and FunctionalEquation to pull in supporting lemmas for the T5 context. The result is a compact public interface for the cost-theoretic core.
why it matters in Recognition Science
The module feeds the CostLayer in DimensionalConstraints.CostLayer, which packages the public cost core for the dimensional constraints rebuttal. It supplies the analyticity and classification results required at the T5 step of the forcing chain, ensuring J-uniqueness rests on the Aczel smoothness theorem for the d'Alembert kernel.
scope and limits
- Does not prove the d'Alembert equation from Recognition axioms.
- Does not classify discontinuous solutions.
- Does not derive the parameter λ from the phi-ladder.
- Does not include mass formulas or Berry thresholds.
used by (1)
depends on (3)
declarations in this module (10)
-
structure
AczelRegularityKernel -
def
aczelRegularityKernel -
theorem
aczel_kernel_smooth -
theorem
aczel_kernel_ode -
structure
PrimitiveCostHypotheses -
theorem
H_one_of_normalized -
theorem
H_continuous_of_positive_continuous -
theorem
H_dAlembert_of_composition -
theorem
primitive_to_uniqueness_of_kernel -
theorem
primitive_to_uniqueness_aczel