CalibrationFromUnitChoice

formal source

  75  strict_convex : StrictConvexOn ℝ (Set.Ioi 0) J
  76
  77/-- Calibration obligation extracted from the unit-choice seam. -/
  78structure CalibrationFromUnitChoice (J : ℝ → ℝ) : Prop where
  79  calibration : (deriv (deriv (fun t => J (Real.exp t)))) 0 = 1
  80
  81/-- Explicit split version of the regularity seam.
  82
  83Instead of a single broad `RegularityCert`, the reconstruction theorem now
  84tracks continuity, convexity, and calibration as independently auditable
  85obligations. -/
  86structure FiniteDescriptionRegularity (J : ℝ → ℝ) : Prop where
  87  continuity : ContinuityFromFiniteDescription J
  88  convexity : StrictConvexityFromClosure J
  89  calibration : CalibrationFromUnitChoice J
  90
  91/-- Fold the split finite-description obligations back into the legacy bundle. -/
  92def FiniteDescriptionRegularity.toRegularityCert {J : ℝ → ℝ}
  93    (h : FiniteDescriptionRegularity J) : RegularityCert J where
  94  continuous := h.continuity.continuous
  95  strict_convex := h.convexity.strict_convex
  96  calibration := h.calibration.calibration
  97
  98/-- Unfold the legacy regularity bundle into the split obligations. -/
  99def RegularityCert.toFiniteDescriptionRegularity {J : ℝ → ℝ}
 100    (h : RegularityCert J) : FiniteDescriptionRegularity J where
 101  continuity := ⟨h.continuous⟩
 102  convexity := ⟨h.strict_convex⟩
 103  calibration := ⟨h.calibration⟩
 104
 105/-- **R6 as theorem**: Compositional closure follows from continuity.
 106If J is continuous on R_{>0}, then J(xy) + J(x/y) is finite. -/
 107theorem composition_from_continuity
 108    (J : ℝ → ℝ)