theorem Frourio.right_epsilon_delta_at_point {φ : ℝ → ℝ} {ε : ℝ} (t : ℝ) (hDini : DiniUpperE φ t ≤ 0) (hε : 0 < ε) : ∃ δ > 0, ∀ (h : ℝ), 0 < h → h < δ → φ (t + h) - φ t ≤ ε * h

Step 1 - Lemma R0: Right ε–δ from Dini If DiniUpperE φ t ≤ 0 and ε > 0, then there exists δ > 0 such that for all 0 < h < δ, we have φ(t+h) - φ(t) ≤ ε·h.

theorem Frourio.uniformization_near_center {φ : ℝ → ℝ} {s r ε w : ℝ} (hw : w ∈ Set.Icc 0 r) (hr : 0 < r) (hDini : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (hUSC : ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (hε : 0 < ε) : ∃ ρ_w > 0, ∃ δ_w > 0, ∀ (y h : ℝ), |y - w| < ρ_w → 0 < h → h < δ_w → quotient_function φ s y h ≤ ε

Step 2 - Lemma U1: Uniformization near w Given R0 at each point near w and upper semicontinuity of the quotient function, we get uniform bounds near w.

theorem Frourio.directed_two_point_control_from_uniformization {φ : ℝ → ℝ} {s r ε w ρ_w δ_w : ℝ} (h_uniform : ∀ (y h : ℝ), |y - w| < ρ_w → 0 < h → h < δ_w → quotient_function φ s y h ≤ ε) (y z : ℝ) : y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → |y - w| < ρ_w → |z - w| < ρ_w → z - y < δ_w → φ (s + z) - φ (s + y) ≤ ε * (z - y)

Step 3 - Lemma U2: Directed two-point control From uniform bounds on the quotient, get the two-point estimate.

theorem Frourio.metric_bridge (y w ρ : ℝ) : |y - w| < ρ ↔ dist y w < ρ

Metric bridge: Convert between absolute value and distance

theorem Frourio.dist_eq_diff_for_ordered {y z : ℝ} (h : y ≤ z) : dist y z = z - y

For y ≤ z, dist y z = z - y

theorem Frourio.lebesgue_uniform_small_interval {φ : ℝ → ℝ} {s r ε : ℝ} (hr : 0 < r) (h_local : ∀ w ∈ Set.Icc 0 r, ∃ ρ_w > 0, ∃ δ_w > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → dist y w < ρ_w → dist z w < ρ_w → z - y < δ_w → φ (s + z) - φ (s + y) ≤ ε * (z - y)) : ∃ L > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → z - y < L → φ (s + z) - φ (s + y) ≤ ε * (z - y)

Step 4 - Lemma L1: Lebesgue-uniform small-interval control

theorem Frourio.lebesgue_number_for_directed_cover_complete {φ : ℝ → ℝ} {s r ε : ℝ} (hDini : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (hUSC : ∀ w ∈ Set.Icc 0 r, ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (hε : 0 < ε) (hr : 0 < r) : ∃ L > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → z - y < L → φ (s + z) - φ (s + y) ≤ ε * (z - y)

Main Theorem: Complete Lebesgue number for directed two-point cover Combining all steps to provide the complete solution.

theorem Frourio.lebesgue_number_for_directed_cover_fixed {φ : ℝ → ℝ} {s r ε : ℝ} (hDini : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (hUSC : ∀ w ∈ Set.Icc 0 r, ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (hε : 0 < ε) (hr : 0 < r) : ∃ L > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → z - y < L → φ (s + z) - φ (s + y) ≤ ε * (z - y)

Alternative formulation matching EVICore6's signature exactly