Kernel
plain-language theorem explainer
Kernel supplies the type of the ILG effective source function as a map from two real arguments to a real value. ILG modelers and resonance-gravity researchers cite it when rewriting the Poisson source term via the pressure variable p = ρ w(k,a) δ. The declaration is a direct type alias with no further content or computation.
Claim. The kernel is the function type $K : ℝ → ℝ → ℝ$ that carries the effective source $4π G a² ρ w δ$ in the ILG pressure display.
background
The module presents ILG as an algebraic pressure display: the effective source is rewritten with pressure variable p := ρ · w(k,a) · δ while the underlying physics remains unchanged. Upstream results supply the constant G in two forms: the RS-native expression λ_rec² c³ / (π ℏ) from Constants and the log-coordinate J-cost G(t) = cosh(t) − 1 from JCostInflaton. The YM.OS.Kernel structure provides a contrasting transfer-kernel example on lattice measures.
proof idea
One-line type abbreviation that directly equates Kernel to the binary real function type ℝ → ℝ → ℝ.
why it matters
The abbreviation supplies the type used by eightTickKernelParams, kernel_at_ratio_one_alpha_zero and kernel_ge_one in ILG.Kernel, and by no_retuning_consistent in CoerciveProjection. It completes the ILG pressure-display scaffold that links the eight-tick octave and resonance conditions to the gravitational source term in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.