  67  calibration : (deriv (deriv (fun t => J (Real.exp t)))) 0 = 1
  68
  69/-- Continuity obligation extracted from the finite-description seam. -/
  70structure ContinuityFromFiniteDescription (J : ℝ → ℝ) : Prop where
  71  continuous : ContinuousOn J (Set.Ioi 0)
  72
  73/-- Strict-convexity obligation extracted from closure/no-arbitrage. -/
  74structure StrictConvexityFromClosure (J : ℝ → ℝ) : Prop where
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.