TransferOperator
plain-language theorem explainer
The TransferOperator extracts the continuous linear map T packaged inside a Kernel structure, yielding an operator on complex functions over lattice measures. Lattice field theorists constructing transfer operators for positivity analyses would cite this when setting up spectral bounds. It is realized by a direct one-line field projection from the Kernel input.
Claim. For a transfer kernel $K$, the associated transfer operator is the continuous linear map $T_K: (M_0 → ℂ) →_L (M_0 → ℂ)$, where $M_0$ denotes the space of lattice measures.
background
LatticeMeasure supplies an abstract interface for measures on lattices. Kernel is the structure that contains a single field T, itself a continuous linear map from complex observables on LatticeMeasure to itself. The module YM.OS assembles these objects to support Osterwalder-Schrader positivity surrogates via uniform overlap bounds.
proof idea
One-line wrapper that returns the T field of the input Kernel.
why it matters
This definition supplies the basic operator whose spectral gap and positivity properties are examined in the same module. It feeds constructions that encode Dobrushin-type contraction compatible with the Recognition Science forcing chain, though no downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.