IndisputableMonolith.Cost.AczelClassification

   1import IndisputableMonolith.Cost.AczelTheorem
   2import IndisputableMonolith.Cost.AczelProof
   3import IndisputableMonolith.Cost.FunctionalEquation
   4
   5namespace IndisputableMonolith
   6namespace Cost
   7namespace FunctionalEquation
   8
   9/-!
  10# Aczel Classification Package
  11
  12This module packages the part of the d'Alembert forcing chain that is supplied
  13by the Aczel classification theorem:
  14
  151. continuous d'Alembert solutions are smooth;
  162. once smoothness is available, the calibrated ODE kernel `H'' = H` follows.
  17
  18The downstream exclusivity code can depend on this kernel without touching the
  19raw Aczel axiom directly.
  20-/
  21
  22/-- The theorem-level payload extracted from the Aczel classification seam. -/
  23structure AczelRegularityKernel (H : ℝ → ℝ) : Prop where
  24  smooth : dAlembert_continuous_implies_smooth_hypothesis H
  25  ode : dAlembert_to_ODE_hypothesis H
  26
  27/-- The default kernel obtained from the current Aczél smoothness package. -/
  28noncomputable def aczelRegularityKernel [AczelSmoothnessPackage] (H : ℝ → ℝ) :
  29    AczelRegularityKernel H where
  30  smooth := dAlembert_smooth_of_aczel H
  31  ode := by
  32    intro h_one h_cont h_dAlembert h_d2_zero
  33    have h_smooth : ContDiff ℝ ⊤ H :=
  34      dAlembert_smooth_of_aczel H h_one h_cont h_dAlembert
  35    exact dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
  36
  37/-- Convenience projection: the smoothness theorem exported by the kernel. -/
  38theorem aczel_kernel_smooth [AczelSmoothnessPackage] (H : ℝ → ℝ) :
  39    dAlembert_continuous_implies_smooth_hypothesis H :=
  40  (aczelRegularityKernel H).smooth
  41
  42/-- Convenience projection: the ODE kernel exported by the classification step. -/
  43theorem aczel_kernel_ode [AczelSmoothnessPackage] (H : ℝ → ℝ) :
  44    dAlembert_to_ODE_hypothesis H :=
  45  (aczelRegularityKernel H).ode
  46
  47/-- Canonical public T5 input bundle.
  48
  49This is the primitive-to-uniqueness route exposed to the rest of the public RS
  50surface. `JensenSketch` remains available as a compatibility layer, but the
  51official statement now records the reciprocal-cost, normalization, composition,
  52calibration, and continuity assumptions explicitly. -/
  53structure PrimitiveCostHypotheses (F : ℝ → ℝ) : Prop where
  54  reciprocal : IsReciprocalCost F
  55  normalized : IsNormalized F
  56  composition : SatisfiesCompositionLaw F
  57  calibrated : IsCalibrated F
  58  continuous : ContinuousOn F (Set.Ioi 0)
  59
  60private theorem H_one_of_normalized (F : ℝ → ℝ)
  61    (hNorm : IsNormalized F) : H F 0 = 1 := by
  62  have h0 : F 1 = 0 := by simpa [IsNormalized] using hNorm
  63  simp [H, G, h0]
  64
  65private theorem H_continuous_of_positive_continuous (F : ℝ → ℝ)
  66    (hCont : ContinuousOn F (Set.Ioi 0)) : Continuous (H F) := by
  67  have h := ContinuousOn.comp_continuous hCont Real.continuous_exp
  68  have h' : Continuous (fun t => F (Real.exp t)) :=
  69    h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
  70  have h_add : Continuous (fun t : ℝ => F (Real.exp t) + (1 : ℝ)) :=
  71    h'.add (continuous_const : Continuous fun _ : ℝ => (1 : ℝ))
  72  simpa [H, G] using h_add
  73
  74private theorem H_dAlembert_of_composition (F : ℝ → ℝ)
  75    (hComp : SatisfiesCompositionLaw F) :
  76    ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u := by
  77  let Gf : ℝ → ℝ := G F
  78  have h_direct : DirectCoshAdd Gf :=
  79    CoshAddIdentity_implies_DirectCoshAdd F ((composition_law_equiv_coshAdd F).mp hComp)
  80  intro t u
  81  have hG := h_direct t u
  82  have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
  83    calc
  84      (Gf (t + u) + 1) + (Gf (t - u) + 1)
  85          = (Gf (t + u) + Gf (t - u)) + 2 := by ring
  86      _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by
  87            simpa [Gf] using hG
  88      _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
  89  simpa [Gf, H, G] using h_goal
  90
  91/-- Official public T5 theorem with an explicit Aczél kernel seam.
  92
  93The public statement now takes the primitive cost hypotheses directly and uses
  94`AczelRegularityKernel` as the sole regularity bridge. This makes the T5 seam
  95explicit without routing through `JensenSketch`. -/
  96theorem primitive_to_uniqueness_of_kernel (F : ℝ → ℝ)
  97    (hF : PrimitiveCostHypotheses F)
  98    (hKernel : AczelRegularityKernel (H F)) :
  99    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 100  have h_H0 : H F 0 = 1 := H_one_of_normalized F hF.normalized
 101  have h_H_cont : Continuous (H F) :=
 102    H_continuous_of_positive_continuous F hF.continuous
 103  have h_H_dAlembert : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u :=
 104    H_dAlembert_of_composition F hF.composition
 105  have h_smooth : ContDiff ℝ ⊤ (H F) :=
 106    hKernel.smooth h_H0 h_H_cont h_H_dAlembert
 107  exact washburn_uniqueness F
 108    hF.reciprocal hF.normalized hF.composition hF.calibrated hF.continuous
 109    hKernel.smooth hKernel.ode
 110    (ode_regularity_continuous_of_smooth h_smooth)
 111    (ode_regularity_differentiable_of_smooth h_smooth)
 112    (ode_regularity_bootstrap_of_smooth h_smooth)
 113
 114/-- Convenience form of the canonical T5 theorem using the current Aczél
 115smoothness package to supply the regularity kernel automatically. -/
 116theorem primitive_to_uniqueness_aczel [AczelSmoothnessPackage] (F : ℝ → ℝ)
 117    (hF : PrimitiveCostHypotheses F) :
 118    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
 119  primitive_to_uniqueness_of_kernel F hF (aczelRegularityKernel (H F))
 120
 121end FunctionalEquation
 122end Cost
 123end IndisputableMonolith
 124