IndisputableMonolith.Foundation.JCostHessianC7

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# C7: Local J-Cost Expansion at Equilibrium
   6
   7The plan originally asked for a Hessian theorem at r = 1. Rather than invoke
   8Mathlib's derivative API, this module proves the exact local algebraic kernel:
   9
  10  J(1 + eps) = eps^2 / (2(1 + eps)).
  11
  12This is stronger than the second-order Taylor claim away from eps = -1. It
  13also records the formal Taylor coefficient 1/2, so the Hessian coefficient is
  141 in the usual normalization.
  15
  16Lean status: 0 sorry, 0 axiom.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace JCostHessianC7
  22
  23open Cost
  24
  25theorem jcost_one_plus_eq (eps : ℝ) (h : eps ≠ -1) :
  26    Jcost (1 + eps) = eps ^ 2 / (2 * (1 + eps)) := by
  27  have hx : 1 + eps ≠ 0 := by
  28    intro hz
  29    apply h
  30    linarith
  31  rw [Jcost_eq_sq hx]
  32  ring_nf
  33
  34/-- The exact quadratic numerator in the local J-cost expansion. -/
  35theorem jcost_local_quadratic_kernel (eps : ℝ) (h : eps ≠ -1) :
  36    Jcost (1 + eps) * (2 * (1 + eps)) = eps ^ 2 := by
  37  rw [jcost_one_plus_eq eps h]
  38  have hx : 1 + eps ≠ 0 := by
  39    intro hz
  40    apply h
  41    linarith
  42  have hden : 2 * (1 + eps) ≠ 0 := by
  43    exact mul_ne_zero (by norm_num) hx
  44  field_simp [hden, hx]
  45
  46/-- Taylor coefficient at equilibrium: J(1+eps) has leading term eps^2 / 2. -/
  47noncomputable def jcostTaylorQuadraticCoefficient : ℝ := 1 / 2
  48
  49theorem jcostTaylorQuadraticCoefficient_eq :
  50    jcostTaylorQuadraticCoefficient = 1 / 2 := rfl
  51
  52/-- In the standard Taylor convention, Hessian = 2 * quadratic coefficient. -/
  53noncomputable def jcostHessianCoefficient : ℝ :=
  54  2 * jcostTaylorQuadraticCoefficient
  55
  56theorem jcostHessianCoefficient_eq_one :
  57    jcostHessianCoefficient = 1 := by
  58  unfold jcostHessianCoefficient jcostTaylorQuadraticCoefficient
  59  norm_num
  60
  61structure JCostHessianCert where
  62  local_kernel : ∀ eps : ℝ, eps ≠ -1 →
  63    Jcost (1 + eps) * (2 * (1 + eps)) = eps ^ 2
  64  coefficient_half : jcostTaylorQuadraticCoefficient = 1 / 2
  65  hessian_one : jcostHessianCoefficient = 1
  66
  67def jcostHessianCert : JCostHessianCert where
  68  local_kernel := jcost_local_quadratic_kernel
  69  coefficient_half := jcostTaylorQuadraticCoefficient_eq
  70  hessian_one := jcostHessianCoefficient_eq_one
  71
  72end JCostHessianC7
  73end Foundation
  74end IndisputableMonolith
  75