FG Core: Frourio Geometry core API

This module introduces the minimal core types for Frourio Geometry (FG) as per design phase G1, generalizing to the m-point calibration setting while staying proof-light and non-destructive to existing analysis code.

Provided here:

• FGData: geometric/analytic data on a metric-measure space.
• ScaleAction: abstract scale action with isometry/similarity toggles and quasi-invariance/homogeneity predicates.
• toEVI: bridge from FGData to the existing EVIProblem.
• effectiveLambda: helper for similarity scaling of the EVI parameter.

FG data on a metric-measure space with an energy and auxiliary operators. This is intentionally lightweight: Γ, Γ₂ are abstract endomorphisms to keep the API flexible at this phase.

structure Frourio.FGData (X : Type u_1) [PseudoMetricSpace X] [MeasurableSpace X] : Type u_1

• μ : MeasureTheory.Measure X
• E : X → ℝ
• Γ : (X → ℝ) → X → ℝ
• Γ₂ : (X → ℝ) → X → ℝ
• lam : ℝ

def Frourio.FGData.toEVI {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) : EVIProblem X

Equations

• FG.toEVI = { E := FG.E, lam := FG.lam }

Scale action skeleton. The fields are Prop-valued to capture requirements without committing to concrete constructions yet.

• Λ: scale factor (typically Λ > 1; the positivity/large-ness is asserted via separate predicates, not as fields here). • act: integer-parameterized action k ↦ S_{Λ^k} on X. • isometry: declares the action is isometric (α = 0 scenario). • similarity: declares similarity with an exponent α. • measure_quasiInvariant: pushforward relation (S_k)_# μ = θ_k μ. • generator_homogeneous: generator scaling exponent κ.

structure Frourio.ScaleAction (X : Type u_1) : Type u_1

• Lambda : ℝ
• act : ℤ → X → X
• isometry : Prop
• similarity : ℝ → Prop
• measure_quasiInvariant (k : ℤ) : Prop
• generator_homogeneous : ℝ → Prop

Effective EVI parameter under similarity scaling. For a similarity with exponent α and generator homogeneity exponent κ, the effective EVI parameter at scale k is Λ^{(κ - 2α) k} · λ. We model the real power via Real.rpow and coerce k : ℤ into ℝ.

noncomputable def Frourio.effectiveLambda (α κ Λ : ℝ) (k : ℤ) (lam : ℝ) : ℝ

Equations

• Frourio.effectiveLambda α κ Λ k lam = Real.exp ((κ - 2 * α) * ↑k * Real.log Λ) * lam