TransferOperator
The TransferOperator extracts the continuous linear map T from a Kernel record to act on complex observables over an abstract lattice measure space. Lattice model researchers building Osterwalder-Schrader positivity or spectral gap arguments would cite this extraction when assembling transfer kernels. The definition reduces to a direct field projection from the Kernel structure.
claimFor a transfer kernel $K$, the associated transfer operator is the continuous linear map $T_K: (L(M) → ℂ) →_L (L(M) → ℂ)$, where $L(M)$ denotes the space of functions on the lattice measure and $→_L$ denotes continuous linear maps over $ℂ$.
background
LatticeMeasure supplies an abstract interface for lattice measures in the YM.OS module. Kernel is the structure that packages a single field T, the continuous linear operator acting on complex observables over this measure space. The module imports Mathlib to support the linear algebra and topology required for the codomain type.
proof idea
The definition is a one-line wrapper that projects the T field from the supplied Kernel instance.
why it matters in Recognition Science
This definition supplies the transfer operator required by sibling constructions such as OSPOSitivity and MassGap in the same module. It supports the Recognition Science program of deriving spectral positivity from kernel structures, consistent with the phi-ladder and discrete tiering seen in upstream results like NucleosynthesisTiers. No open questions are closed here.
scope and limits
- Does not specify any explicit action of the kernel on observables.
- Does not enforce positivity, contraction, or spectral gap properties.
- Does not reference Recognition Science constants such as phi or K.
- Does not address continuum limits or renormalization.
formal statement (Lean)
25noncomputable def TransferOperator (K : Kernel) : (LatticeMeasure → ℂ) →L[ℂ] (LatticeMeasure → ℂ) :=
proof body
Definition body.
26 K.T
27
28/-- OS reflection positivity surrogate: existence of a transfer kernel with a
29 uniform overlap lower bound β ∈ (0,1]. This encodes a spectral positivity
30 guard compatible with Dobrushin-type contraction. -/