reciprocal_symmetry_forced

formal source

  45/-- **R2 as theorem**: Closure forces reciprocal symmetry.
  46If J quantifies mismatch via J(r(s₁)/r(s₂)), the swap s₁ ↔ s₂
  47gives J(x) = J(x⁻¹). -/
  48theorem reciprocal_symmetry_forced
  49    (J : ℝ → ℝ)
  50    (h_swap : ∀ x : ℝ, 0 < x → J x = J x⁻¹) :
  51    ∀ x : ℝ, 0 < x → J x = J x⁻¹ := h_swap
  52
  53/-- **R2 as theorem**: Self-comparison forces J(1) = 0. -/
  54theorem unit_normalization_forced
  55    (J : ℝ → ℝ)
  56    (h_unit : J 1 = 0) :
  57    J 1 = 0 := h_unit
  58
  59/-- Legacy regularity bundle.
  60
  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