FiniteDescriptionRegularity

formal source

  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 : ℝ → ℝ)
 109    (hJ_cont : ContinuousOn J (Set.Ioi 0))
 110    (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
 111    ∃ v : ℝ, J (x * y) + J (x / y) = v :=
 112  ⟨J (x * y) + J (x / y), rfl⟩
 113
 114/-- **Ledger Reconstruction Theorem**: A closed observable framework
 115canonically carries a zero-parameter comparison ledger.
 116R1, R2, R5, R6 are proved; the remaining seam is tracked as three explicit