`IndisputableMonolith.URCAdapters.ELProp`

IndisputableMonolith/URCAdapters/ELProp.lean · 22 lines · 2 declarations

Explainer status: ready · generated 2026-05-16 16:28:32.363688+00:00

   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

source mirrored from github.com/jonwashburn/shape-of-logic