comparison_symm

formal source

  39theorem comparison_irrefl (F : ClosedObservableFramework) (s : F.S) :
  40    ¬ (F.r s ≠ F.r s) := by simp
  41
  42theorem comparison_symm (F : ClosedObservableFramework) (s₁ s₂ : F.S) :
  43    F.r s₁ ≠ F.r s₂ → F.r s₂ ≠ F.r s₁ := Ne.symm
  44
  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