kernelAtRefK_eq
plain-language theorem explainer
The lemma establishes equality between the ILG reference kernel at unit wave number and the general kernel function for any parameter bundle P and scale factor a. Researchers deriving scale-dependent corrections in cosmology or coercivity bounds would cite it to reduce expressions at the reference point. The proof is a direct term-mode simplification that unfolds the two kernel definitions and applies the arithmetic identity for multiplication by one.
Claim. For a parameter bundle $P$ consisting of exponent $alpha$, amplitude $C$, and positive reference timescale $tau_0$, and for any real scale factor $a$, the reference kernel satisfies $w(1,a)=w(P,1,a)$.
background
The ILG module defines the kernel $w(k,a)=1+C(a/(k tau_0))^alpha$ with $alpha=(1-1/phi)/2$. KernelParams bundles the exponent, amplitude, reference timescale, and the proof that $tau_0>0$. The general kernel function appears in the BIT kernel families as a case distinction over constant, inverse-linear, and exponential families, while the ILG version specializes the same form. The module documentation lists reduction to unity at the reference scale as one of the four main results.
proof idea
One-line term proof that applies the simplifier to the definitions of the reference kernel and the general kernel, together with the theorem that multiplication by one is the identity.
why it matters
The result supplies an automatic simplification rule inside the ILG kernel development. It directly implements the module claim that the kernel reduces to 1 at the reference scale and supports the subsequent monotonicity and coercivity statements. In the Recognition Science setting it anchors the self-similar fixed-point behavior at the eight-tick octave reference, ensuring consistent forcing-chain evaluation when the wave number is normalized to unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.