IndisputableMonolith.Verification.JcostSatisfiesJensenCert

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace JcostSatisfiesJensen
   7
   8open IndisputableMonolith.Cost
   9
  10/-!
  11# Jcost Satisfies JensenSketch Certificate
  12
  13This certificate closes the T5 uniqueness loop by proving that **Jcost itself**
  14satisfies the `JensenSketch` interface requirements.
  15
  16## Why this matters
  17
  18The T5 uniqueness theorem (`T5UniqueCert`) states:
  19> Any function F satisfying `JensenSketch` equals `Jcost` on (0, ∞).
  20
  21But this is conditional on F satisfying `JensenSketch`. This certificate proves:
  22> `Jcost` satisfies all `JensenSketch` requirements.
  23
  24Together, these establish:
  251. If F satisfies JensenSketch, then F = Jcost (T5 uniqueness)
  262. Jcost satisfies JensenSketch requirements (this certificate)
  273. Therefore, Jcost is THE unique cost function satisfying these axioms
  28
  29## JensenSketch Requirements
  30
  31The `JensenSketch` class requires:
  321. **Symmetry**: F(x) = F(1/x) for x > 0
  332. **Unit normalization**: F(1) = 0
  343. **Axis upper bound**: F(exp t) ≤ J(exp t) for all t
  354. **Axis lower bound**: J(exp t) ≤ F(exp t) for all t
  36
  37For Jcost, requirements 3-4 are trivially satisfied (equality holds by `rfl`),
  38and 1-2 are proven from the explicit formula J(x) = (x + x⁻¹)/2 - 1.
  39
  40## Proof
  41
  42The proof is definitional: Jcost's symmetry and unit normalization are
  43algebraically verified, and the axis bounds are reflexive equalities.
  44-/
  45
  46structure JcostSatisfiesJensenCert where
  47  deriving Repr
  48
  49/-- Verification predicate: Jcost satisfies all JensenSketch requirements.
  50
  51This certifies all four JensenSketch requirements for Jcost:
  521. Jcost(x) = Jcost(1/x) for x > 0 (symmetry)
  532. Jcost(1) = 0 (unit normalization)
  543. Jcost(exp t) ≤ Jcost(exp t) for all t (axis upper - trivial)
  554. Jcost(exp t) ≤ Jcost(exp t) for all t (axis lower - trivial)
  56-/
  57@[simp] def JcostSatisfiesJensenCert.verified (_c : JcostSatisfiesJensenCert) : Prop :=
  58  -- Jcost satisfies all JensenSketch requirements
  59  (∀ x : ℝ, 0 < x → Jcost x = Jcost x⁻¹) ∧
  60  (Jcost 1 = 0) ∧
  61  (∀ t : ℝ, Jcost (Real.exp t) ≤ Jcost (Real.exp t)) ∧
  62  (∀ t : ℝ, Jcost (Real.exp t) ≤ Jcost (Real.exp t))
  63
  64/-- Top-level theorem: the certificate verifies.
  65
  66This proves Jcost satisfies JensenSketch requirements, closing the T5 uniqueness loop. -/
  67@[simp] theorem JcostSatisfiesJensenCert.verified_any (c : JcostSatisfiesJensenCert) :
  68    JcostSatisfiesJensenCert.verified c := by
  69  refine ⟨?symm, ?unit, ?upper, ?lower⟩
  70  · -- Symmetry: Jcost(x) = Jcost(1/x)
  71    intro x hx
  72    exact Jcost_symm hx
  73  · -- Unit normalization: Jcost(1) = 0
  74    exact Jcost_unit0
  75  · -- Axis upper bound (trivial equality)
  76    intro t
  77    exact le_refl _
  78  · -- Axis lower bound (trivial equality)
  79    intro t
  80    exact le_refl _
  81
  82/-- The Jcost instance can be explicitly constructed from the verified properties. -/
  83def jcost_jensen_sketch : JensenSketch Jcost :=
  84  { symmetric := fun hx => Jcost_symm hx
  85  , unit0 := Jcost_unit0
  86  , axis_upper := fun _ => le_refl _
  87  , axis_lower := fun _ => le_refl _ }
  88
  89end JcostSatisfiesJensen
  90end Verification
  91end IndisputableMonolith
  92