FG Theorems: Statement-only wrappers

This module provides statement-level definitions (Prop-valued) that tie the FG core data to the existing analysis layer (EVI/Doob/Mosco), as outlined in design phase G2. Proofs and quantitative details are left to later phases; here we fix API shapes and dependencies.

def Frourio.evi_scale_rule {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) (S : ScaleAction X) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Frourio.evi_scale_rule_isometry {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) (S : ScaleAction X) (hIso : S.isometry) (hκ : ∃ (κ : ℝ), S.generator_homogeneous κ) : evi_scale_rule FG S

Isometry scale rule (theoremized skeleton).

Sketch: In the isometric case, take α = 0. Under generator homogeneity with exponent κ, the effective parameter becomes lam' = effectiveLambda 0 κ S.Lambda k FG.lam = exp((κ k) log Λ) · lam. Here we only assert the existence of such α, κ and the algebraic form of lam' via the effectiveLambda helper; quantitative EVI preservation is handled in later phases.

theorem Frourio.evi_scale_rule_similarity {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) (S : ScaleAction X) (α : ℝ) (hSim : S.similarity α) (hκ : ∃ (κ : ℝ), S.generator_homogeneous κ) : evi_scale_rule FG S

Similarity scale rule (theoremized skeleton).

Sketch: In the similarity case with exponent α, and generator homogeneity exponent κ, the EVI parameter rescales according to lam' = effectiveLambda α κ S.Lambda k FG.lam. This statement packages the existence of the pair (α, κ) and the algebraic form via effectiveLambda; the full EVI preservation is treated in subsequent proof phases.

def Frourio.mosco_inheritance {ι : Type u_1} (S : MoscoSystem ι) : Prop

Equations

• Frourio.mosco_inheritance S = Frourio.EVILimitHolds S

theorem Frourio.mosco_inheritance_thm {ι : Type u_1} (S : MoscoSystem ι) (H : MoscoAssumptions S) : mosco_inheritance S

Mosco inheritance theoremized via the analysis-layer eviInheritance.

noncomputable def Frourio.cStarCoeff (_σ : ℝ) : ℝ

Placeholder coefficient c_* (σ) controlling the ‖S_m‖_∞^2 contribution.

Equations

• Frourio.cStarCoeff _σ = 0

noncomputable def Frourio.cDCoeff (_σ : ℝ) : ℝ

Placeholder coefficient c_D (σ) controlling the ‖Ξ_m‖ contribution.

Equations

• Frourio.cDCoeff _σ = 0

noncomputable def Frourio.budgetFromSigma (σ : ℝ) : ConstantBudget

Build the analysis‑layer budget from the m‑point coefficients at scale σ.

Equations

• Frourio.budgetFromSigma σ = { cStar := Frourio.cStarCoeff σ, cD := Frourio.cDCoeff σ }

noncomputable def Frourio.budgetFromSigmaWithFlag (σ : ℝ) (comm : Bool) : ConstantBudget

Boolean toggle for commutative-design simplification at scale σ. When comm = true, the c_* contribution is set to 0 in the assembled budget.

Equations

• Frourio.budgetFromSigmaWithFlag σ comm = { cStar := if comm = true then 0 else Frourio.cStarCoeff σ, cD := Frourio.cDCoeff σ }

theorem Frourio.budgetFromSigmaWithFlag_comm_true (σ : ℝ) : (budgetFromSigmaWithFlag σ true).cStar = 0 ∧ (budgetFromSigmaWithFlag σ true).cD = cDCoeff σ

theorem Frourio.budgetFromSigmaWithFlag_comm_false (σ : ℝ) : (budgetFromSigmaWithFlag σ false).cStar = (budgetFromSigma σ).cStar ∧ (budgetFromSigmaWithFlag σ false).cD = (budgetFromSigma σ).cD

theorem Frourio.budget_commutative_simplify (σ : ℝ) : ∃ (B : ConstantBudget), B.cStar = 0 ∧ B.cD = cDCoeff σ

Statement-level link: under a commutative-design regime, one may set c_* (σ) = 0 in the budget assembly. This is kept as a Prop-level lemma for downstream use; quantitative proofs are deferred.

noncomputable def Frourio.cStarCoeff_model (kStar σ : ℝ) : ℝ

A simple model for the m‑point coefficients. Tunable gains k*, kD produce nonnegative coefficients depending on σ.

Equations

• Frourio.cStarCoeff_model kStar σ = kStar * σ ^ 2

noncomputable def Frourio.cDCoeff_model (kD σ : ℝ) : ℝ

Equations

• Frourio.cDCoeff_model kD σ = kD * |σ|

theorem Frourio.cStarCoeff_model_nonneg {kStar σ : ℝ} (hk : 0 ≤ kStar) : 0 ≤ cStarCoeff_model kStar σ

theorem Frourio.cDCoeff_model_nonneg {kD σ : ℝ} (hk : 0 ≤ kD) : 0 ≤ cDCoeff_model kD σ

noncomputable def Frourio.budgetFromSigmaModel (kStar kD σ : ℝ) : ConstantBudget

Assemble a budget from the model.

Equations

• Frourio.budgetFromSigmaModel kStar kD σ = { cStar := Frourio.cStarCoeff_model kStar σ, cD := Frourio.cDCoeff_model kD σ }

theorem Frourio.budgetFromSigmaModel_nonneg {kStar kD σ : ℝ} (hks : 0 ≤ kStar) (hkd : 0 ≤ kD) : 0 ≤ (budgetFromSigmaModel kStar kD σ).cStar ∧ 0 ≤ (budgetFromSigmaModel kStar kD σ).cD

theorem Frourio.lambdaEffLowerBound_from_sigma_model {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (lam eps Ssup XiNorm σ kStar kD : ℝ) : lambdaEffLowerBound A (budgetFromSigmaModel kStar kD σ) lam eps (lambdaBE lam eps - A.gamma * ((budgetFromSigmaModel kStar kD σ).cStar * Ssup ^ 2 + (budgetFromSigmaModel kStar kD σ).cD * XiNorm)) Ssup XiNorm

Supply an explicit lambdaEffLowerBound using the model budget. The witness is the canonical right-hand side value.

theorem Frourio.flow_suite_from_packs {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (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

Integrated suite corollary: from weak hypothesis flags and an equivalence assumption pack for F := Ent + γ·Dσm with λ_BE := lambdaBE S.base.lam S.eps, plus a packaged lower bound and a two‑EVI hypothesis, we obtain the three gradient-flow conclusions.

theorem Frourio.flow_suite_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)) (B : AnalyticBridges 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 built from consolidated analytic flags and bridge statements for the PLFA↔EDE, EDE↔EVI, and JKO⇒PLFA components. Prefer this variant when you already work at the analytic-flags level.

theorem Frourio.flow_suite_from_flags_and_ede_evi_pack {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)) (P : EDEEVIAssumptions S.func.F (lambdaBE S.base.lam S.eps)) (HjkoPlfa : JKO_PLFA_from_analytic_flags 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

Proof-backed variant: use analytic flags and an EDEEVIAssumptions pack to construct the equivalence package, then assemble the integrated suite.

theorem Frourio.tensorization_min_rule_thm {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [PseudoMetricSpace Y] [MeasurableSpace Y] (S₁ : GradientFlowSystem X) (S₂ : GradientFlowSystem Y) (hK1₁ : K1prime S₁.func) (hK1₂ : K1prime S₂.func) (hγ₁ : 0 ≤ S₁.func.gamma) (hγ₂ : 0 ≤ S₂.func.gamma) : tensorization_min_rule S₁ S₂

Tensorization (min rule) theoremized: if both factors satisfy the coercivity surrogate K1prime and have nonnegative couplings, then the combined system satisfies the statement-level tensorization predicate.

theorem Frourio.ede_evi_pred_for_FG {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (HC : HalfConvex S.func.F (lambdaBE S.base.lam S.eps)) (SUB : StrongUpperBound S.func.F) (H : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) : EDE_EVI_pred S.func.F (lambdaBE S.base.lam S.eps)

Step 1 (FG-level wrapper): from λ-semi-convexity and a strong upper bound for F := Ent + γ·Dσm with λ_eff := lambdaBE λ ε, together with an analytic bridge statement EDE_EVI_from_analytic_flags, obtain the component predicate EDE_EVI_pred (i.e., EDE ⇔ EVI(λ_eff)) for all curves.

theorem Frourio.ede_to_evi_for_FG {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (HC : HalfConvex S.func.F (lambdaBE S.base.lam S.eps)) (SUB : StrongUpperBound S.func.F) (H : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) : EDE_to_EVI_from_flags S.func.F (lambdaBE S.base.lam S.eps)

Convenience: FG-level directional bridge (EDE → EVI) from analytic flags. Wraps ede_to_evi_from_flags_auto at the GradientFlowSystem level.

theorem Frourio.evi_to_ede_for_FG {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (HC : HalfConvex S.func.F (lambdaBE S.base.lam S.eps)) (SUB : StrongUpperBound S.func.F) (H : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) : EVI_to_EDE_from_flags S.func.F (lambdaBE S.base.lam S.eps)

Convenience: FG-level directional bridge (EVI → EDE) from analytic flags.

theorem Frourio.ede_evi_pack_for_FG {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (HC : HalfConvex S.func.F (lambdaBE S.base.lam S.eps)) (SUB : StrongUpperBound S.func.F) (H : EDE_EVI_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) : EDEEVIAssumptions S.func.F (lambdaBE S.base.lam S.eps)

Step 1 (FG-level pack): the same as ede_evi_pred_for_FG, but packaged as EDEEVIAssumptions for downstream assembly into the equivalence.

theorem Frourio.plfa_ede_pred_for_FG {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (A : AnalyticFlags S.func.F (lambdaBE S.base.lam S.eps)) (H : PLFA_EDE_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) : PLFA_EDE_pred S.func.F

Step 3 (FG-level wrapper): from analytic flags for F := Ent + γ·Dσm with λ_eff := lambdaBE λ ε and a PLFA⇔EDE analytic bridge, obtain the component predicate PLFA_EDE_pred (i.e., PLFA ⇔ EDE) for all curves.

theorem Frourio.plfa_ede_pack_for_FG {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (A : AnalyticFlags S.func.F (lambdaBE S.base.lam S.eps)) (H : PLFA_EDE_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) : PLFAEDEAssumptions S.func.F

Step 3 (FG-level pack): the same as plfa_ede_pred_for_FG, but packaged as PLFAEDEAssumptions for downstream assembly into the equivalence.

Concrete sufficient conditions (FG-side, statement-level)

We provide lightweight constructors to obtain analytic flags and bridge packs for F := Ent + γ·Dσm with λ_eff := lambdaBE λ ε, from FG-side assumptions. The content remains statement-level until analytic proofs are added.

theorem Frourio.analytic_flags_for_FG {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (_HK1 : K1prime S.func) (_HK4 : K4m S.func) : AnalyticFlags S.func.F (lambdaBE S.base.lam S.eps)

Produce AnalyticFlags for F := Ent + γ·Dσm (statement-level). We accept minimal inputs (K1prime, K4m) and build the flags.