theorem Frourio.eviSynchronizationSq_no_error {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (_geodesicBetween : Prop) (Hsum0 : eviSumNoError P u v hu hv _geodesicBetween) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) : ContractionPropertySq P u v

Synchronization in squared distance (no error) via homogeneous Grönwall. Takes the mixed half-form inequality with η = 0, upgrades it to the DiniUpper W + (2λ) W ≤ 0 form, and applies the homogeneous Grönwall predicate.

theorem Frourio.twoEVI_sq_from_sum {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (geodesicBetween : Prop) (Hsum0 : eviSumNoError P u v hu hv geodesicBetween) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) : ContractionPropertySq P u v

two‑EVI (no error): squared-distance synchronization from the mixed half-form sum inequality and a homogeneous Grönwall lemma.

theorem Frourio.twoEVI_dist_from_sum {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (geodesicBetween : Prop) (Hsum0 : eviSumNoError P u v hu hv geodesicBetween) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) (Hbridge : Hbridge P u v) : ContractionProperty P u v

two‑EVI (no error): distance synchronization using a homogeneous Grönwall lemma and a bridge from squared to linear distances.

theorem Frourio.evi_synchronization_thm_concrete {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (geodesicBetween : Prop) (Hsum0 : eviSumNoError P u v hu hv geodesicBetween) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) : ContractionProperty P u v

End-to-end (no error): from a mixed half-form EVI sum and a homogeneous Gronwall predicate, obtain the distance-version synchronization via the concrete bridge.

def Frourio.ContractionPropertyWithError {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (η : ℝ) : Prop

Distance-version synchronization with error. From the squared-distance bound and algebraic sqrt identities, derive

dist(u t, v t) ≤ exp (-(P.lam) t) · dist(u 0, v 0) + √(max 0 ((2 η) t)).

We use max 0 to keep the radicand nonnegative when η t < 0.

Equations

• Frourio.ContractionPropertyWithError P u v η = ∀ (t : ℝ), dist (u t) (v t) ≤ Real.exp (-P.lam * t) * dist (u 0) (v 0) + √(max 0 (2 * η * t))

def Frourio.HbridgeWithError {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (η : ℝ) : Prop

Error-bridge predicate from squared to linear distance with an error term.

Equations

• Frourio.HbridgeWithError P u v η = (Frourio.ContractionPropertySqWithError P u v η → Frourio.ContractionPropertyWithError P u v η)

theorem Frourio.bridge_with_error {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (η : ℝ) (H : HbridgeWithError P u v η) (Hsq : ContractionPropertySqWithError P u v η) : ContractionPropertyWithError P u v η

Wrapper: apply a provided error-bridge to convert squared to linear distance.

theorem Frourio.twoEVI_sq_with_error_from_sum {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (geodesicBetween : Prop) (hR : MixedErrorBound X u v) (Hsum : eviSumWithError P u v hu hv geodesicBetween hR) (Hgr : gronwall_exponential_contraction_with_error_half_pred P.lam hR.η fun (t : ℝ) => d2 (u t) (v t)) : ContractionPropertySqWithError P u v hR.η

two‑EVI (with external force): squared-distance synchronization from a single mixed EVI sum hypothesis and an inhomogeneous Grönwall lemma.

theorem Frourio.twoEVI_with_error_dist_from_sum {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (geodesicBetween : Prop) (hR : MixedErrorBound X u v) (Hsum : eviSumWithError P u v hu hv geodesicBetween hR) (Hgr : gronwall_exponential_contraction_with_error_half_pred P.lam hR.η fun (t : ℝ) => d2 (u t) (v t)) (Hbridge : HbridgeWithError P u v hR.η) : ContractionPropertyWithError P u v hR.η

two‑EVI (with external force): distance synchronization with error from a single mixed sum hypothesis, an inhomogeneous Grönwall lemma, and a bridge.

theorem Frourio.bridge_contraction_with_error_concrete {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (η : ℝ) : HbridgeWithError P u v η

Concrete error-bridge: from squared-distance synchronization with error to distance-version with error, using √(x + y) ≤ √x + √y and the algebraic identities for √(exp) and √(a·b).

theorem Frourio.HbridgeWithError_concrete_all_eta {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (η : ℝ) : HbridgeWithError P u v η

Provide a concrete with‑error bridge for all error levels η by reusing the explicit square‑root algebra above.

theorem Frourio.evi_synchronization_with_error_thm_concrete {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (geodesicBetween : Prop) (hR : MixedErrorBound X u v) (Hsum : eviSumWithError P u v hu hv geodesicBetween hR) (Hgr : (∀ (t : ℝ), 1 / 2 * DiniUpper (fun (τ : ℝ) => d2 (u τ) (v τ)) t + P.lam * d2 (u t) (v t) ≤ hR.η) → ∀ (t : ℝ), d2 (u t) (v t) ≤ Real.exp (-(2 * P.lam) * t) * d2 (u 0) (v 0) + 2 * hR.η * t) : ContractionPropertyWithError P u v hR.η

End-to-end: from a mixed EVI sum and an inhomogeneous Grönwall helper, obtain the distance-version synchronization with error via the concrete bridge.