IndisputableMonolith.Cost.AczelClass

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Cost
   5namespace FunctionalEquation
   6
   7open Real
   8
   9/-! # AczelSmoothnessPackage Class
  10
  11This module declares the typeclass interface for the d'Alembert smoothness
  12package and the bootstrap theorem that uses it. The class is a typeclass-style
  13hypothesis carrier; concrete instances live in
  14`IndisputableMonolith.Cost.AczelProof`.
  15
  16History: pre-2026-04-25 the class was declared in the curated public-release
  17sibling `RecognitionScience/Cost/AczelTheorem.lean`. The 2026-04-25 RS↔IM
  18consolidation kept the larger IM `AczelTheorem.lean` (the unconditional proof)
  19and the larger RS `FunctionalEquation.lean` (the typeclass-parameterized
  20Washburn uniqueness theorem). This split file decouples the class declaration
  21from both, so neither has to depend on the other.
  22-/
  23
  24/-- Aczél smoothness requirement: continuous d'Alembert solutions are C^∞.
  25
  26Any continuous solution of H(t+u) + H(t-u) = 2·H(t)·H(u) with H(0) = 1
  27is infinitely differentiable.
  28
  29Mathematical basis (Aczél 1966, Ch. 3): the complete classification is
  301. H(t) = 1 (constant, trivially C^∞)
  312. H(t) = cosh(λt), λ ≠ 0 (C^∞)
  323. H(t) = cos(λt), λ ≠ 0 (C^∞)
  33
  34A concrete `instance` is provided in `IndisputableMonolith.Cost.AczelProof`
  35via the unconditional `dAlembert_contDiff_top` theorem in
  36`IndisputableMonolith.Cost.AczelTheorem`. -/
  37class AczelSmoothnessPackage : Prop where
  38  smooth_of_dAlembert :
  39    ∀ (H : ℝ → ℝ),
  40      H 0 = 1 →
  41      Continuous H →
  42      (∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) →
  43      ContDiff ℝ ⊤ H
  44
  45/-- Smoothness of continuous d'Alembert solutions, parameterized by an
  46`AczelSmoothnessPackage` instance. -/
  47theorem aczel_dAlembert_smooth [AczelSmoothnessPackage] (H : ℝ → ℝ)
  48    (h_one : H 0 = 1)
  49    (h_cont : Continuous H)
  50    (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
  51    ContDiff ℝ ⊤ H :=
  52  AczelSmoothnessPackage.smooth_of_dAlembert H h_one h_cont h_dAlembert
  53
  54end FunctionalEquation
  55end Cost
  56end IndisputableMonolith
  57