EVI → EDE: Regularity‑aware minimal results

This file provides small, provable implications from EVI to EDE under strong regularity assumptions, removing previous unprovable placeholders.

theorem Frourio.evi_to_ede_constant {X : Type u_1} (F : X → ℝ) (x : X) (ρ : ℝ → X) (hconst : ∀ (t : ℝ), ρ t = x) : EDE F ρ

theorem Frourio.evi_to_ede_with_reg {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) (hLocConst : ∀ (t : ℝ), ∃ δ > 0, ∀ (h : ℝ), 0 < h ∧ h < δ → ρ (t + h) = ρ t) : EDE F ρ