AczelRegularityKernel

formal source

  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