aczelRegularityKernel

formal source

  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)