aczel_kernel_smooth

formal source

  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)) :=