TransferOperator
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.