kernelAtRefK_eq
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove positivity of the kernel for arbitrary parameter choices.
- Does not derive the numerical value of alpha from the self-similarity fixed point.
- Does not address the Berry creation threshold or the phi-ladder mass formula.
- Does not establish monotonicity with respect to the scale factor.
formal statement (Lean)
86@[simp] lemma kernelAtRefK_eq (P : KernelParams) (a : ℝ) :
87 kernelAtRefK P a = kernel P 1 a := by
proof body
Term-mode proof.
88 simp [kernelAtRefK, kernel, one_mul]
89
90/-! ## Basic Properties -/
91
92/-- Kernel is always positive for valid parameters. -/