IndisputableMonolith.Verification.ConvexityCert

   1import Mathlib
   2import IndisputableMonolith.Cost.Convexity
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace Convexity
   7
   8open IndisputableMonolith.Cost
   9open Real Set
  10
  11/-!
  12# Convexity Certificate: Strict Convexity (A3)
  13
  14This certificate packages the proofs that cosh and Jlog are strictly convex,
  15which is axiom A3 in the uniqueness theorem T5.
  16
  17## Key Results
  18
  191. `StrictConvexOn ℝ univ Real.cosh` — cosh is strictly convex on ℝ
  202. `StrictConvexOn ℝ univ Jlog` — Jlog is strictly convex on ℝ
  213. `StrictConvexOn ℝ (Ioi 0) Jcost` — Jcost is strictly convex on ℝ₊
  22
  23## Why this matters for the certificate chain
  24
  25Strict convexity guarantees that:
  26- The minimum at the origin is unique
  27- No other cost function with the same symmetry properties can exist
  28- The cost function is bowl-shaped with a single global minimum
  29
  30The proof uses the second derivative test:
  31- cosh''(t) = cosh(t) > 0 for all t
  32- Therefore cosh is strictly convex
  33- Jlog = cosh - 1, so Jlog inherits strict convexity
  34
  35## Mathematical Content
  36
  37For Jcost on ℝ₊:
  38- J''(x) = x⁻³ > 0 for x > 0
  39- Therefore Jcost is strictly convex on (0, ∞)
  40-/
  41
  42structure ConvexityCert where
  43  deriving Repr
  44
  45/-- Verification predicate: cosh and Jlog are strictly convex.
  46
  47This certifies:
  481. cosh is strictly convex on ℝ
  492. Jlog is strictly convex on ℝ
  503. Jcost is strictly convex on (0, ∞) -/
  51@[simp] def ConvexityCert.verified (_c : ConvexityCert) : Prop :=
  52  -- cosh is strictly convex on ℝ
  53  StrictConvexOn ℝ univ Real.cosh ∧
  54  -- Jlog is strictly convex on ℝ
  55  StrictConvexOn ℝ univ Jlog ∧
  56  -- Jcost is strictly convex on (0, ∞)
  57  StrictConvexOn ℝ (Ioi (0 : ℝ)) Jcost
  58
  59/-- Top-level theorem: the certificate verifies. -/
  60@[simp] theorem ConvexityCert.verified_any (c : ConvexityCert) :
  61    ConvexityCert.verified c := by
  62  refine ⟨?_, ?_, ?_⟩
  63  · exact cosh_strictly_convex
  64  · exact Jlog_strictConvexOn
  65  · exact Jcost_strictConvexOn_pos
  66
  67end Convexity
  68end Verification
  69end IndisputableMonolith
  70