theorem Frourio.analytic_bridges_from_component_packs {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (Hplfa_ede : PLFAEDEAssumptions S.func.F) (Hede_evi : EDEEVIAssumptions S.func.F (lambdaBE S.base.lam S.eps)) (Hjko_plfa : JKOPLFAAssumptions S.func.F) : AnalyticBridges S.func.F (lambdaBE S.base.lam S.eps)

Build AnalyticBridges from component packs for F := Ent + γ·Dσm. Given the three component packs, we promote them to analytic-flag bridges by ignoring the flag inputs (statement-level).

theorem Frourio.analytic_bridges_from_equiv_pack {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (H : EquivBuildAssumptions S.func.F (lambdaBE S.base.lam S.eps)) : AnalyticBridges S.func.F (lambdaBE S.base.lam S.eps)

Build AnalyticBridges from an equivalence-assumption pack.

theorem Frourio.flow_suite_from_flags {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (A : AnalyticFlags S.func.F (lambdaBE S.base.lam S.eps)) (Hpack : EquivBuildAssumptions S.func.F (lambdaBE S.base.lam S.eps)) (hLam : lambdaEffLowerBound S.func S.budget S.base.lam S.eps (lambdaBE S.base.lam S.eps) S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Bridge-eliminated variant: given analytic flags and an equivalence pack for F := Ent + γ·Dσm with λ_eff := lambdaBE λ ε, synthesize the analytic bridges internally and conclude the integrated suite. This replaces the bridge propositions by explicit constructions.

theorem Frourio.flow_suite_from_concrete_conditions {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (_HK1 : K1prime S.func) (_HK4 : K4m S.func) (Hplfa_ede : PLFAEDEAssumptions S.func.F) (Hede_evi : EDEEVIAssumptions S.func.F (lambdaBE S.base.lam S.eps)) (Hjko_plfa : JKOPLFAAssumptions S.func.F) (hLam : lambdaEffLowerBound S.func S.budget S.base.lam S.eps (lambdaBE S.base.lam S.eps) S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Integrated suite from concrete component packs and minimal FG flags.

theorem Frourio.flow_suite_from_fg_flags_and_equiv {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (_HK1 : K1prime S.func) (_HK4 : K4m S.func) (Hpack : EquivBuildAssumptions S.func.F (lambdaBE S.base.lam S.eps)) (hLam : lambdaEffLowerBound S.func S.budget S.base.lam S.eps (lambdaBE S.base.lam S.eps) S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Fully bridged variant: starting from minimal FG flags K1′/K4^m and an equivalence pack for F := Ent + γ·Dσm, synthesize both the analytic flags and bridges internally and conclude the integrated suite.

theorem Frourio.flow_suite_from_doob_mpoint {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (Hpack : EquivBuildAssumptions S.func.F (lambdaBE S.base.lam S.eps)) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Integrated suite via Doob + m-point assumptions: constructs the effective-λ lower bound using the functional-layer wrapper and then applies flow_suite_from_packs. This moves the lower-bound input from a raw assumption to a theorem-backed construction.

theorem Frourio.flow_suite_from_real_flags {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (flags : AnalyticFlagsReal X S.func.F (lambdaBE S.base.lam S.eps)) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis S.func.F ρ) (HplfaEde : PLFA_EDE_from_real_flags S.func.F (lambdaBE S.base.lam S.eps)) (HedeEvi_builder : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) (HjkoPlfa : JKO_PLFA_from_real_flags S.func.F (lambdaBE S.base.lam S.eps)) (hLam : lambdaEffLowerBound S.func S.budget S.base.lam S.eps (lambdaBE S.base.lam S.eps) S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Integrated suite via real analytic flags and the MM (real) route. Given real analytic flags for F := Ent + γ·Dσm with λ_eff := lambdaBE λ ε, and the three real-route bridges (PLFA⇔EDE, EDE⇔EVI via placeholder builder, and JKO⇒PLFA), conclude the gradient-flow equivalence, effective-λ lower bound, and two‑EVI with force.

theorem Frourio.flow_suite_from_real_flags_auto {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (flags : AnalyticFlagsReal X S.func.F (lambdaBE S.base.lam S.eps)) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis S.func.F ρ) (HedeEvi_builder : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) (hLam : lambdaEffLowerBound S.func S.budget S.base.lam S.eps (lambdaBE S.base.lam S.eps) S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Convenience: same as flow_suite_from_real_flags but automatically supplies the real-route bridges using PLFACore builders. Only the EDE⇔EVI builder must be provided.

theorem Frourio.lamLower_from_real_flags {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (flags : AnalyticFlagsReal X S.func.F (lambdaBE S.base.lam S.eps)) : ∃ (L : ℝ), lambdaBE S.base.lam S.eps ≥ L

Supply the explicit numeric lower bound from real flags as a pair (L, lamEff ≥ L). This is a light-weight accessor independent of the budgeted inequality.

theorem Frourio.equivalence_from_real_flags_auto {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (flags : AnalyticFlagsReal X S.func.F (lambdaBE S.base.lam S.eps)) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis S.func.F ρ) (HedeEvi_builder : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) : plfaEdeEviJko_equiv S.func.F (lambdaBE S.base.lam S.eps)

Build the core equivalence PLFA = EDE = EVI = JKO for F := Ent + γ·Dσm with λ_eff := lambdaBE λ ε from real analytic flags, supplying the PLFA↔EDE and JKO→PLFA real-route bridges automatically.

theorem Frourio.equivalence_from_flags_and_bridges {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (A : AnalyticFlags S.func.F (lambdaBE S.base.lam S.eps)) (HplfaEde : PLFA_EDE_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) (HedeEvi : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) (HjkoPlfa : JKO_PLFA_from_analytic_flags S.func.F) : plfaEdeEviJko_equiv S.func.F (lambdaBE S.base.lam S.eps)

Build the core equivalence from placeholder analytic flags and explicit component builders (PLFA↔EDE, EDE⇔EVI builder, JKO→PLFA).

theorem Frourio.equivalence_from_equiv_pack {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (H : EquivBuildAssumptions S.func.F (lambdaBE S.base.lam S.eps)) : plfaEdeEviJko_equiv S.func.F (lambdaBE S.base.lam S.eps)

Build the core equivalence from an EquivBuildAssumptions pack directly.

def Frourio.flow_equivalence {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : Prop

Re-export: gradient-flow equivalence (PLFA = EDE = EVI = JKO).

Equations

• Frourio.flow_equivalence S = Frourio.gradient_flow_equiv S

def Frourio.lambda_eff_lower {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : Prop

Re-export: effective lambda lower bound statement.

Equations

• Frourio.lambda_eff_lower S = Frourio.lambda_eff_lower_bound S

theorem Frourio.lambda_eff_lower_from_doob {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : lambda_eff_lower S

Convenience: construct lambda_eff_lower from Doob assumptions and m‑point zero‑order bounds using the analysis‑layer constructive inequality.

def Frourio.two_evi_with_force_alias {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : Prop

Re-export: two-EVI with external force (squared-distance synchronization).

Equations

• Frourio.two_evi_with_force_alias S = Frourio.two_evi_with_force S

def Frourio.evi_multiscale_rule {m : ℕ} (Λ α κ : Fin m → ℝ) (k : Fin m → ℤ) : Prop

Multiscale EVI parameter rule alias (m-dimensional scale composition).

Equations

• Frourio.evi_multiscale_rule Λ α κ k = Frourio.multiscale_lambda_rule Λ α κ k

theorem Frourio.two_evi_with_force_to_distance_concrete {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (Htwo : two_evi_with_force S) (u v : ℝ → X) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred S.base.lam η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError { E := S.func.F, lam := S.base.lam } u v η

Distance synchronization with error (concrete route): From two_evi_with_force S and a Grönwall predicate for W(t) = d2(u t, v t), obtain a distance synchronization statement with an explicit error η. This wraps twoEVIWithForce_to_distance_concrete.

theorem Frourio.two_evi_with_force_to_distance_concrete_closed {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (Htwo : two_evi_with_force S) (u v : ℝ → X) (Hgr_all : ∀ (η : ℝ), gronwall_exponential_contraction_with_error_half_pred S.base.lam η fun (t : ℝ) => d2 (u t) (v t)) : ∃ (η : ℝ), ContractionPropertyWithError { E := S.func.F, lam := S.base.lam } u v η

Closed distance synchronization (concrete route): if the Grönwall predicate holds for all η, then two_evi_with_force S yields a distance synchronization bound without additional inputs. Wraps twoEVIWithForce_to_distance_concrete_closed.