FG8 A3: K-transform skeleton and basic model

This module introduces a lightweight KTransform structure capturing the multi-point transform 𝒦_σ as a map into (signed) kernels on ℝ together with minimal predicates representing (K1′) narrow continuity and (K4^m) geodesic affinity. A 1D basic model is provided to serve as a concrete instance. The design remains proof-light and avoids measure-theoretic load.

structure Frourio.KTransform (X : Type u_2) [PseudoMetricSpace X] : Type u_2

K-transform: a map attaching to each state x : X a kernel on ℝ. The payload is an arbitrary function ℝ → ℝ at this phase.

• map : X → ℝ → ℝ
• narrowContinuous : Prop

def Frourio.K1primeK {X : Type u_1} [PseudoMetricSpace X] (K : KTransform X) : Prop

(K1′) surrogate: narrow continuity predicate.

Equations

• Frourio.K1primeK K = K.narrowContinuous

def Frourio.UniformLowerBoundAtZero {X : Type u_1} [PseudoMetricSpace X] (K : KTransform X) (C0 : ℝ) : Prop

Auxiliary predicate: a uniform lower bound for the kernel at s = 0. This lightweight surrogate is used to produce coercivity-style bounds for Dσm when building the functional layer.

Equations

• Frourio.UniformLowerBoundAtZero K C0 = ∀ (x : X), K.map x 0 ≥ -C0

noncomputable def Frourio.DsigmamFromK {X : Type u_1} [PseudoMetricSpace X] (K : KTransform X) (Ssup : ℝ) : X → ℝ

Interface: build Dσm from a KTransform and a supplied sup-norm bound. We keep it algebraic via a simple evaluation map x 0, scaled by Ssup.

Equations

• Frourio.DsigmamFromK K Ssup x = Ssup * K.map x 0

Basic boundedness helper for DsigmamFromK

theorem Frourio.DsigmamFromK_lower_bound {X : Type u_1} [PseudoMetricSpace X] (K : KTransform X) (Ssup C0 : ℝ) (hS : 0 ≤ Ssup) (hLB : UniformLowerBoundAtZero K C0) (x : X) : DsigmamFromK K Ssup x ≥ -(Ssup * C0)

Uniform lower bound for Dσm inherited from the kernel lower bound at s=0.

General templates to supply (K1′) beyond the basic example. These are lightweight builders that keep narrow continuity as a Prop-level flag, while offering convenient ways to construct KTransforms from pointwise continuity-in-x hypotheses and functorial pullbacks.

def Frourio.PointwiseContinuousInX {X : Type u_1} [PseudoMetricSpace X] (map : X → ℝ → ℝ) : Prop

Pointwise continuity in the state variable x (for each s ∈ ℝ).

Equations

• Frourio.PointwiseContinuousInX map = ∀ (s : ℝ), Continuous fun (x : X) => map x s

structure Frourio.K1primeTemplate (X : Type u_2) [PseudoMetricSpace X] : Type u_2

A template capturing map together with a pointwise continuity witness.

• map : X → ℝ → ℝ
• pointwise_cont : PointwiseContinuousInX self.map

def Frourio.K1primeTemplate.pullback {X : Type u_1} [PseudoMetricSpace X] {Y : Type u_2} [PseudoMetricSpace Y] (T : K1primeTemplate X) (g : Y → X) (hg : Continuous g) : K1primeTemplate Y

Pull back a template along a continuous map g : Y → X to obtain a template on Y. This preserves pointwise continuity-in-x.

Equations

• T.pullback g hg = { map := fun (y : Y) (s : ℝ) => T.map (g y) s, pointwise_cont := ⋯ }

def Frourio.KTransform.pullback {X : Type u_1} [PseudoMetricSpace X] {Y : Type u_2} [PseudoMetricSpace Y] (K : KTransform X) (g : Y → X) : KTransform Y

Functorial builder: pull back a KTransform along g : Y → X. The narrowContinuous flag is transported unchanged as a Prop.

Equations

• K.pullback g = { map := fun (y : Y) (s : ℝ) => K.map (g y) s, narrowContinuous := K.narrowContinuous }

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

• interp : X → X → ℝ → X
• endpoint0 (x y : X) : self.interp x y 0 = x
• endpoint1 (x y : X) : self.interp x y 1 = y

def Frourio.DisplacementAffinity {X : Type u_1} [PseudoMetricSpace X] (K : KTransform X) (D : Displacement X) : Prop

Displacement affinity (K4^m) surrogate: along the displacement interpolation, evaluation of the kernel is affine in x for each fixed s.

Equations

• Frourio.DisplacementAffinity K D = ∀ (x y : X), ∀ θ ∈ Set.Icc 0 1, ∀ (s : ℝ), K.map (D.interp x y θ) s = (1 - θ) * K.map x s + θ * K.map y s

noncomputable def Frourio.linearDisplacement : Displacement ℝ

Equations

• Frourio.linearDisplacement = { interp := fun (x y θ : ℝ) => (1 - θ) * x + θ * y, endpoint0 := Frourio.linearDisplacement._proof_1, endpoint1 := Frourio.linearDisplacement._proof_2 }

noncomputable def Frourio.Displacement.pullback {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (D : Displacement X) (f : X → Y) (g : Y → X) (hfg : ∀ (y : Y), f (g y) = y) : Displacement Y

Pull back a displacement along g : Y → X using a (one‑sided) section f : X → Y with g ∘ f = id (or along an equivalence).

Equations

• D.pullback f g hfg = { interp := fun (y1 y2 : Y) (θ : ℝ) => f (D.interp (g y1) (g y2) θ), endpoint0 := ⋯, endpoint1 := ⋯ }

theorem Frourio.Displacement.pullback_compat {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (D : Displacement X) (f : X → Y) (g : Y → X) (hfg : ∀ (y : Y), f (g y) = y) (hgf : ∀ (x : X), g (f x) = x) (y1 y2 : Y) (θ : ℝ) : θ ∈ Set.Icc 0 1 → g ((D.pullback f g hfg).interp y1 y2 θ) = D.interp (g y1) (g y2) θ

The pullback displacement is compatible with the original via the maps.