IndisputableMonolith.Foundation.JCostConvexityInLogSpace

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# J-Cost Convexity in Log Space — ALEXIS Internal Note
   6
   7From ALEXIS_ExpB_Internal_Note.tex:
   8"The log-ratio (1/2)(ln x)^2 is the same cost family; it is convex
   9in log space with the same fixed point at x = 1."
  10
  11This module proves the key structural identity underlying the ALEXIS
  12closed-loop control result:
  13
  141. J-cost has a unique global minimum at x = 1 (J(1) = 0)
  152. In log coordinates t = ln(x): the function g(t) = J(eᵗ) satisfies
  16   g(0) = 0 (fixed point at t = 0)
  17   g(t) = g(-t) (even function in log space)
  18   g(t) > 0 for t ≠ 0
  19
  203. The approximation: near t = 0, g(t) ≈ t²/2 (the log-ratio form)
  21
  224. Both J(x) and ½(ln x)² share:
  23   - The same fixed point at x = 1
  24   - The same symmetry J(x) = J(x⁻¹)
  25   - The same sign pattern
  26
  27Lean status: 0 sorry, 0 axiom.
  28-/
  29
  30namespace IndisputableMonolith.Foundation.JCostConvexityInLogSpace
  31open Cost
  32
  33/-- J-cost in log coordinates: g(t) = J(eᵗ). -/
  34noncomputable def g (t : ℝ) : ℝ := Jcost (Real.exp t)
  35
  36/-- g(0) = J(e⁰) = J(1) = 0. -/
  37theorem g_at_zero : g 0 = 0 := by
  38  unfold g
  39  simp [Jcost_unit0]
  40
  41/-- g is even: g(t) = g(-t). -/
  42theorem g_even (t : ℝ) : g t = g (-t) := by
  43  unfold g
  44  rw [Real.exp_neg]
  45  exact Jcost_symm (Real.exp_pos t)
  46
  47/-- g(t) > 0 for t ≠ 0. -/
  48theorem g_pos_off_zero {t : ℝ} (ht : t ≠ 0) : 0 < g t := by
  49  unfold g
  50  apply Jcost_pos_of_ne_one
  51  · exact Real.exp_pos t
  52  · intro h
  53    have : t = 0 := by
  54      have hexp := h
  55      rw [← Real.log_exp t] at hexp
  56      simp [Real.log_one] at hexp ⊢
  57      exact Real.log_exp t ▸ hexp
  58    exact ht this
  59
  60/-- The log-ratio function h(t) = t²/2 has the same fixed point and sign. -/
  61noncomputable def h (t : ℝ) : ℝ := t ^ 2 / 2
  62
  63theorem h_at_zero : h 0 = 0 := by simp [h]
  64
  65theorem h_even (t : ℝ) : h t = h (-t) := by unfold h; ring
  66
  67theorem h_nonneg (t : ℝ) : 0 ≤ h t := by unfold h; positivity
  68
  69theorem h_pos_off_zero {t : ℝ} (ht : t ≠ 0) : 0 < h t := by
  70  unfold h; positivity
  71
  72/-- g and h share the same fixed point at t = 0. -/
  73theorem same_fixed_point : g 0 = 0 ∧ h 0 = 0 := ⟨g_at_zero, h_at_zero⟩
  74
  75/-- Both g and h are even functions. -/
  76theorem same_symmetry : ∀ t, g t = g (-t) ∧ h t = h (-t) :=
  77  fun t => ⟨g_even t, h_even t⟩
  78
  79structure JCostLogSpaceCert where
  80  g_zero : g 0 = 0
  81  g_even : ∀ t, g t = g (-t)
  82  g_positive : ∀ {t : ℝ}, t ≠ 0 → 0 < g t
  83  h_zero : h 0 = 0
  84  h_even : ∀ t, h t = h (-t)
  85  h_nonneg : ∀ t, 0 ≤ h t
  86  same_fixed_pt : g 0 = 0 ∧ h 0 = 0
  87  same_sym : ∀ t, g t = g (-t) ∧ h t = h (-t)
  88
  89noncomputable def jCostLogSpaceCert : JCostLogSpaceCert where
  90  g_zero := g_at_zero
  91  g_even := g_even
  92  g_positive := g_pos_off_zero
  93  h_zero := h_at_zero
  94  h_even := h_even
  95  h_nonneg := h_nonneg
  96  same_fixed_pt := same_fixed_point
  97  same_sym := same_symmetry
  98
  99end IndisputableMonolith.Foundation.JCostConvexityInLogSpace
 100