Kernel
plain-language theorem explainer
Kernel defines a transfer operator T as a continuous linear map on complex-valued functions over an abstract lattice measure. Researchers establishing operator positivity or resonance conditions in lattice models would cite this when bounding energies or certifying synchronization. The definition supplies the identity operator as the default inhabitant via a direct construction from the continuous linear map library.
Claim. A kernel consists of a continuous linear operator $T: (M → ℂ) →_L (M → ℂ)$, where $M$ is an abstract lattice measure.
background
LatticeMeasure is defined as an abstract structure deriving Inhabited, serving as an interface for lattice measures without concrete realization. The YM.OS module introduces Kernel to capture transfer operators acting on complex observables, consistent with upstream identity constructions in CostAlgebra and kernel functions from BITKernelFamilies and ILG.Kernel. These upstream results supply the identity automorphism and the explicit kernel formula $w(k,a) = 1 + C · (a/(k τ₀))^α$ used to instantiate concrete cases.
proof idea
The structure declaration is direct; the Inhabited instance is a one-line wrapper that applies ContinuousLinearMap.id ℂ (LatticeMeasure → ℂ) to furnish the canonical element.
why it matters
Kernel supplies the operator type required by downstream theorems such as no_retuning_consistent (which bounds energy when w ≥ 1) and eight_tick_resonance_certified (which certifies resonance minima). It also supports ILG.Kernel definitions of eightTickKernelParams and kernel_at_ratio_one_alpha_zero. Within the Recognition framework this aligns with the transfer aspects of the eight-tick octave (T7) and operator positivity needed for the D=3 spatial structure (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.