aczel_kernel_ode

formal source

  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