IndisputableMonolith.URCAdapters.ELProp

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4namespace IndisputableMonolith
   5namespace URCAdapters
   6
   7/-! EL stationarity and minimality on the log axis (extracted).
   8    Re-expose the minimal Prop and witness using the central `Cost` module. -/
   9
  10noncomputable section
  11
  12def EL_prop : Prop :=
  13  (deriv Cost.Jlog 0 = 0) ∧ (∀ t : ℝ, Cost.Jlog 0 ≤ Cost.Jlog t)
  14
  15lemma EL_holds : EL_prop := by
  16  exact ⟨Cost.EL_stationary_at_zero, Cost.EL_global_min⟩
  17
  18end
  19
  20end URCAdapters
  21end IndisputableMonolith
  22