IndisputableMonolith.Verification.ODEFoundationCert

   1import Mathlib
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace ODEFoundation
   7
   8open IndisputableMonolith.Cost.FunctionalEquation
   9open Real
  10
  11/-!
  12# ODE Foundation Certificate: Zero Uniqueness and Even Derivative
  13
  14This certificate packages the foundational ODE uniqueness results that
  15underpin the cosh uniqueness theorem.
  16
  17## Key Results
  18
  191. **ODE Zero Uniqueness**: f'' = f with f(0) = 0, f'(0) = 0 implies f = 0
  202. **Even Derivative Zero**: Even function H differentiable at 0 implies H'(0) = 0
  21
  22## Why this matters for the certificate chain
  23
  24These are the core lemmas that make the ODE cosh uniqueness proof work:
  25
  261. **ODE Zero Uniqueness** shows that homogeneous initial conditions give
  27   the zero solution. This is used to prove cosh uniqueness by taking
  28   H - cosh and showing it's zero.
  29
  302. **Even Derivative Zero** provides the H'(0) = 0 initial condition from
  31   the symmetry (evenness) of the cost function in log-coordinates.
  32
  33The proof of ODE Zero Uniqueness uses a beautiful diagonalization trick:
  34- Write f' - f and f' + f as the "eigencomponents"
  35- These satisfy g' = -g and h' = h respectively
  36- With zero initial conditions, both must be zero
  37- Therefore f = 0
  38
  39## Mathematical Content
  40
  41For g' = -g with g(0) = 0:
  42- Consider g(t) · exp(t), which has zero derivative
  43- So g(t) · exp(t) = g(0) · exp(0) = 0
  44- Therefore g(t) = 0
  45
  46Similarly for h' = h with h(0) = 0.
  47-/
  48
  49structure ODEFoundationCert where
  50  deriving Repr
  51
  52/-- Verification predicate: ODE zero uniqueness and even derivative zero.
  53
  54This certifies:
  551. f'' = f with f(0) = f'(0) = 0 implies f = 0 everywhere
  562. Even H with H differentiable at 0 implies H'(0) = 0 -/
  57@[simp] def ODEFoundationCert.verified (_c : ODEFoundationCert) : Prop :=
  58  -- ODE zero uniqueness
  59  (∀ f : ℝ → ℝ,
  60    ContDiff ℝ 2 f →
  61    (∀ t, deriv (deriv f) t = f t) →
  62    f 0 = 0 →
  63    deriv f 0 = 0 →
  64    ∀ t, f t = 0) ∧
  65  -- Even derivative at zero
  66  (∀ H : ℝ → ℝ,
  67    Function.Even H →
  68    DifferentiableAt ℝ H 0 →
  69    deriv H 0 = 0)
  70
  71/-- Top-level theorem: the certificate verifies. -/
  72@[simp] theorem ODEFoundationCert.verified_any (c : ODEFoundationCert) :
  73    ODEFoundationCert.verified c := by
  74  constructor
  75  · intro f h1 h2 h3 h4
  76    exact ode_zero_uniqueness f h1 h2 h3 h4
  77  · intro H h1 h2
  78    exact even_deriv_at_zero H h1 h2
  79
  80end ODEFoundation
  81end Verification
  82end IndisputableMonolith
  83