IndisputableMonolith.RRF.Models.Quadratic

   1import IndisputableMonolith.RRF.Core
   2import Mathlib.Analysis.InnerProductSpace.Basic
   3import Mathlib.Analysis.InnerProductSpace.EuclideanDist
   4
   5/-!
   6# RRF Models: Quadratic Model
   7
   8A non-trivial model with `State = ℝⁿ` and `J(x) = ‖x‖²`.
   9
  10This demonstrates that RRF structures can model continuous optimization
  11and provides a testing ground for theorems about minimizers.
  12-/
  13
  14
  15namespace IndisputableMonolith
  16namespace RRF.Models
  17
  18open RRF.Core
  19
  20/-! ## The Quadratic Model in ℝ -/
  21
  22/-- 1D Quadratic strain: J(x) = x². -/
  23def quadratic1DStrain : StrainFunctional ℝ where
  24  J := fun x => x ^ 2
  25
  26instance : StrainFunctional.NonNeg quadratic1DStrain where
  27  nonneg := fun x => sq_nonneg x
  28
  29/-- Zero is the unique equilibrium. -/
  30theorem quadratic1D_equilibrium : quadratic1DStrain.isBalanced 0 := by
  31  simp [StrainFunctional.isBalanced, quadratic1DStrain]
  32
  33/-- Zero is the unique equilibrium (uniqueness). -/
  34theorem quadratic1D_unique_equilibrium (x : ℝ) :
  35    quadratic1DStrain.isBalanced x ↔ x = 0 := by
  36  simp [StrainFunctional.isBalanced, quadratic1DStrain]
  37
  38/-- Zero is the global minimizer. -/
  39theorem quadratic1D_minimizer : quadratic1DStrain.isMinimizer 0 := by
  40  intro y
  41  simp [StrainFunctional.weaklyBetter, quadratic1DStrain]
  42  exact sq_nonneg y
  43
  44/-- The quadratic model has a unique minimum. -/
  45theorem quadratic1D_hasUniqueMin : quadratic1DStrain.hasUniqueMin := by
  46  use 0
  47  constructor
  48  · exact quadratic1D_equilibrium
  49  · intro y hy
  50    exact (quadratic1D_unique_equilibrium y).mp hy
  51
  52/-! ## Quadratic Ledger -/
  53
  54/-- A trivial ledger constraint for ℝ (always closed). -/
  55def quadratic1DLedger : LedgerConstraint ℝ where
  56  debit := fun _ => 0
  57  credit := fun _ => 0
  58
  59theorem quadratic1D_ledger_closed (x : ℝ) : quadratic1DLedger.isClosed x := rfl
  60
  61/-- Combined strain-ledger for 1D quadratic. -/
  62def quadratic1DStrainLedger : StrainLedger ℝ where
  63  strain := quadratic1DStrain
  64  ledger := quadratic1DLedger
  65
  66/-- Zero is the unique valid state. -/
  67theorem quadratic1D_zero_valid : quadratic1DStrainLedger.isValid 0 :=
  68  ⟨quadratic1D_equilibrium, quadratic1D_ledger_closed 0⟩
  69
  70/-! ## Quadratic Octave -/
  71
  72/-- Observation channel: identity observation, quality = strain. -/
  73def quadratic1DChannel : DisplayChannel ℝ ℝ where
  74  observe := id
  75  quality := fun x => x ^ 2
  76
  77/-- The 1D quadratic octave. -/
  78def quadratic1DOctave : Octave where
  79  State := ℝ
  80  strain := quadratic1DStrain
  81  channels := {
  82    Index := Unit
  83    Obs := fun _ => ℝ
  84    channel := fun _ => quadratic1DChannel
  85  }
  86  inhabited := ⟨0⟩
  87
  88theorem quadratic1DOctave_wellPosed : quadratic1DOctave.wellPosed :=
  89  ⟨(0 : ℝ), quadratic1D_equilibrium⟩
  90
  91/-! ## Shifted Quadratic (demonstrates argmin invariance) -/
  92
  93/-- Shifted quadratic: J(x) = (x - a)² with minimum at a. -/
  94def shiftedQuadraticStrain (a : ℝ) : StrainFunctional ℝ where
  95  J := fun x => (x - a) ^ 2
  96
  97instance (a : ℝ) : StrainFunctional.NonNeg (shiftedQuadraticStrain a) where
  98  nonneg := fun x => sq_nonneg (x - a)
  99
 100theorem shifted_equilibrium (a : ℝ) : (shiftedQuadraticStrain a).isBalanced a := by
 101  simp [StrainFunctional.isBalanced, shiftedQuadraticStrain]
 102
 103theorem shifted_is_minimizer (a : ℝ) : (shiftedQuadraticStrain a).isMinimizer a := by
 104  intro y
 105  simp [StrainFunctional.weaklyBetter, shiftedQuadraticStrain]
 106  exact sq_nonneg (y - a)
 107
 108/-! ## Quadratic demonstrates monotone argmin invariance -/
 109
 110/-- The exponential transform `exp ∘ J` has the same argmin as `J`.
 111    Proof uses that exp is strictly monotone. -/
 112theorem exp_preserves_argmin (x : ℝ) :
 113    quadratic1DStrain.isMinimizer x →
 114    (∀ y, Real.exp (quadratic1DStrain.J x) ≤ Real.exp (quadratic1DStrain.J y)) := by
 115  intro hx y
 116  exact Real.exp_le_exp.mpr (hx y)
 117
 118end RRF.Models
 119end IndisputableMonolith
 120