TransferKernel
plain-language theorem explainer
TransferKernel packages a continuous linear map T on the space of complex functions indexed by ι as the basic type for transfer operators in the YM kernel layer. Builders of explicit kernels cite it when lifting matrix data to function-space operators via buildKernelFromMatrix. The declaration is a direct structure with a single field holding the bounded linear map over ℂ.
Claim. A transfer kernel on an index set ι is a continuous linear operator T : (ι → ℂ) →_L[ℂ] (ι → ℂ).
background
The YM.Kernel module supplies structures that connect matrix representations to linear operators on function spaces. The signature uses the Mathlib notation →L[ℂ] for continuous linear maps between complex vector spaces. Upstream results supply auxiliary T as the natural-number period in Breath1024 and the triangular number in Gap45, together with ledger objects L that record debit and credit maps in the Recognition and Cycle3 modules.
proof idea
The declaration is a structure definition that directly introduces the field T as the continuous linear map from (ι → ℂ) to itself.
why it matters
TransferKernel is the parent type for buildKernelFromMatrix, which constructs a kernel together with its MatrixBridge, and for kernel3x3_with_bridge, which instantiates the constant stochastic 3x3 case. It supplies the operator interface required by KernelHasMatrixView and MatrixBridge. In the Recognition framework the structure supports transfer operators that appear in cycle and synchronization constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.