RegularityCert

formal source

  61This compatibility structure is kept for downstream users that still expect one
  62record, but the public reconstruction path below now prefers the split
  63finite-description obligations. -/
  64structure RegularityCert (J : ℝ → ℝ) : Prop where
  65  continuous : ContinuousOn J (Set.Ioi 0)
  66  strict_convex : StrictConvexOn ℝ (Set.Ioi 0) J
  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