Bridges part of PLFA/EDE/JKO: EVI-dependent statements and packages. This file places [PseudoMetricSpace X] only where needed.

theorem Frourio.build_EDEEVI_pack_from_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (H : EDE_EVI_from_analytic_flags F lamEff) : EDEEVIAssumptions F lamEff

theorem Frourio.component_predicates_from_analytic_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H1 : PLFA_EDE_from_analytic_flags F lamEff) (H2 : EDE_EVI_from_analytic_flags F lamEff) (H3 : JKO_PLFA_from_analytic_flags F) (A : AnalyticFlags F lamEff) : PLFA_EDE_pred F ∧ EDE_EVI_pred F lamEff ∧ JKO_to_PLFA_pred F

structure Frourio.GlobalSufficientPack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

• HC : HalfConvex F lamEff
• SUB : StrongUpperBound F
• components : PLFA_EDE_pred F ∧ EDE_EVI_pred F lamEff ∧ JKO_to_PLFA_pred F

theorem Frourio.global_sufficient_pack_from_analytic_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H1 : PLFA_EDE_from_analytic_flags F lamEff) (H2 : EDE_EVI_from_analytic_flags F lamEff) (H3 : JKO_PLFA_from_analytic_flags F) (A : AnalyticFlags F lamEff) : GlobalSufficientPack F lamEff

theorem Frourio.build_package_from_global {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : GlobalSufficientPack F lamEff) : plfaEdeEviJko_equiv F lamEff

theorem Frourio.build_package_from_analytic_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H1 : PLFA_EDE_from_analytic_flags F lamEff) (H2 : EDE_EVI_from_analytic_flags F lamEff) (H3 : JKO_PLFA_from_analytic_flags F) (A : AnalyticFlags F lamEff) : plfaEdeEviJko_equiv F lamEff

theorem Frourio.plfaEdeEviJko_equiv_from_core_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (H1 : PLFA_EDE_from_analytic_flags F lamEff) (H2 : EDE_EVI_from_analytic_flags F lamEff) (H3 : JKO_PLFA_from_analytic_flags F) : plfaEdeEviJko_equiv F lamEff

Materialize the full equivalence PLFA = EDE = EVI = JKO from core analytic flags and the three builder routes, without additional bridges.

theorem Frourio.build_package_from_flags_and_directional_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (HplfaEde : PLFA_EDE_from_analytic_flags F lamEff) (Hfwd : EDE_to_EVI_from_flags F lamEff) (Hrev : EVI_to_EDE_from_flags F lamEff) (HjkoPlfa : JKO_PLFA_from_analytic_flags F) : plfaEdeEviJko_equiv F lamEff

Build the full equivalence from analytic flags, using PLFA_EDE and JKO_PLFA builders, and directional bridges to assemble EDE_EVI.

theorem Frourio.global_sufficient_pack_from_directional_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (HplfaEde : PLFA_EDE_from_analytic_flags F lamEff) (Hfwd : EDE_to_EVI_from_flags F lamEff) (Hrev : EVI_to_EDE_from_flags F lamEff) (HjkoPlfa : JKO_PLFA_from_analytic_flags F) : GlobalSufficientPack F lamEff

Global sufficient pack from flags and directional bridges.

theorem Frourio.ede_to_evi_from_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hpred : EDE_EVI_pred F lamEff) : EDE_to_EVI_from_flags F lamEff

Derive the forward directional bridge from a pointwise EDE ⇔ EVI predicate.

theorem Frourio.evi_to_ede_from_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hpred : EDE_EVI_pred F lamEff) : EVI_to_EDE_from_flags F lamEff

Derive the reverse directional bridge from a pointwise EDE ⇔ EVI predicate.

theorem Frourio.ede_to_evi_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : EDE_to_EVI_from_flags F lamEff

Directional bridges from an EDEEVIAssumptions pack (ignores the flags).

theorem Frourio.evi_to_ede_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : EVI_to_EDE_from_flags F lamEff

theorem Frourio.ede_to_evi_from_flags_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags F lamEff) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) : EDE_to_EVI_from_flags F lamEff

Directional bridges from an EDE_EVI_from_analytic_flags builder via flags.

theorem Frourio.evi_to_ede_from_flags_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags F lamEff) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) : EVI_to_EDE_from_flags F lamEff

theorem Frourio.ede_to_evi_from_evi_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EVIBridgeForward (fun (F : X → ℝ) (ρ : ℝ → X) => EDE F ρ) F lamEff) : EDE_to_EVI_from_flags F lamEff

Tie the flags-directional bridge to a generic EVI-side forward bridge predicate.

theorem Frourio.evi_to_ede_from_evi_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EVIBridgeBackward (fun (F : X → ℝ) (ρ : ℝ → X) => EDE F ρ) F lamEff) : EVI_to_EDE_from_flags F lamEff

Tie the flags-directional bridge to a generic EVI-side backward bridge predicate.

theorem Frourio.ede_evi_from_evi_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HF : EVIBridgeForward (fun (F : X → ℝ) (ρ : ℝ → X) => EDE F ρ) F lamEff) (HB : EVIBridgeBackward (fun (F : X → ℝ) (ρ : ℝ → X) => EDE F ρ) F lamEff) : EDE_EVI_from_analytic_flags F lamEff

Fully build EDE_EVI_from_analytic_flags from EVI‑side forward/backward bridges specialized to P := EDE. The flags are not used at this phase but are kept to match the target API.

theorem Frourio.ede_evi_from_evi_equiv_bridge {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EVIEquivBridge (fun (F : X → ℝ) (ρ : ℝ → X) => EDE F ρ) F lamEff) : EDE_EVI_from_analytic_flags F lamEff

Variant: build EDE_EVI_from_analytic_flags from an EVI‑side equivalence bridge, i.e. both directions bundled together.

theorem Frourio.evi_forward_bridge_from_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags F lamEff) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) : EVIBridgeForward (fun (F : X → ℝ) (ρ : ℝ → X) => EDE F ρ) F lamEff

Produce the EVI‑side forward bridge instance from the builder and core flags.

theorem Frourio.evi_backward_bridge_from_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags F lamEff) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) : EVIBridgeBackward (fun (F : X → ℝ) (ρ : ℝ → X) => EDE F ρ) F lamEff

Produce the EVI‑side backward bridge instance from the builder and core flags.

def Frourio.EDE_to_EVI_concrete {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

Concrete EVI‑side forward bridge predicate specialized to P := EDE.

Equations

• Frourio.EDE_to_EVI_concrete F lamEff = Frourio.EVIBridgeForward (fun (F : X → ℝ) (ρ : ℝ → X) => Frourio.EDE F ρ) F lamEff

def Frourio.EVI_to_EDE_concrete {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

Concrete EVI‑side backward bridge predicate specialized to P := EDE.

Equations

• Frourio.EVI_to_EDE_concrete F lamEff = Frourio.EVIBridgeBackward (fun (F : X → ℝ) (ρ : ℝ → X) => Frourio.EDE F ρ) F lamEff

theorem Frourio.ede_evi_from_concrete_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HF : EDE_to_EVI_concrete F lamEff) (HB : EVI_to_EDE_concrete F lamEff) : EDE_EVI_from_analytic_flags F lamEff

Use the concrete EVI‑side bridges to produce the flags‑builder EDE_EVI_from_analytic_flags.

theorem Frourio.ede_to_evi_from_concrete {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HF : EDE_to_EVI_concrete F lamEff) : EDE_to_EVI_from_flags F lamEff

Turn a concrete forward bridge into the flags‑directional bridge.

theorem Frourio.evi_to_ede_from_concrete {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HB : EVI_to_EDE_concrete F lamEff) : EVI_to_EDE_from_flags F lamEff

Turn a concrete backward bridge into the flags‑directional bridge.

theorem Frourio.ede_to_evi_concrete_from_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hpred : EDE_EVI_pred F lamEff) : EDE_to_EVI_concrete F lamEff

Obtain a concrete forward bridge EDE → EVI from a pointwise equivalence predicate.

theorem Frourio.evi_to_ede_concrete_from_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hpred : EDE_EVI_pred F lamEff) : EVI_to_EDE_concrete F lamEff

Obtain a concrete backward bridge EVI → EDE from a pointwise equivalence predicate.

theorem Frourio.ede_to_evi_concrete_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : EDE_to_EVI_concrete F lamEff

Concrete bridges from an EDEEVIAssumptions pack.

theorem Frourio.evi_to_ede_concrete_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : EVI_to_EDE_concrete F lamEff

theorem Frourio.ede_to_evi_concrete_from_global {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) : EDE_to_EVI_concrete F lamEff

Concrete bridges from an equivalence package plfaEdeEviJko_equiv.

theorem Frourio.evi_to_ede_concrete_from_global {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) : EVI_to_EDE_concrete F lamEff

theorem Frourio.ede_to_evi_concrete_from_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (H : EDE_EVI_from_analytic_flags F lamEff) : EDE_to_EVI_concrete F lamEff

Supply a concrete forward bridge from analytic flags and the EDE_EVI_from_analytic_flags builder.

theorem Frourio.evi_to_ede_concrete_from_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (H : EDE_EVI_from_analytic_flags F lamEff) : EVI_to_EDE_concrete F lamEff

Supply a concrete backward bridge from analytic flags and the EDE_EVI_from_analytic_flags builder.

theorem Frourio.ede_evi_from_analytic_flags_via_global {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) : EDE_EVI_from_analytic_flags F lamEff

Final assembly route: if a global equivalence package is available, it induces the desired builder EDE_EVI_from_analytic_flags outright.

theorem Frourio.ede_evi_from_analytic_flags_final {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HF : EDE_to_EVI_concrete F lamEff) (HB : EVI_to_EDE_concrete F lamEff) : EDE_EVI_from_analytic_flags F lamEff

Final assembly route: from concrete EVI‑side bridges (both directions), obtain the builder EDE_EVI_from_analytic_flags.