kernelAtRefK
kernelAtRefK supplies the ILG kernel evaluated at unit wavenumber as one plus amplitude times the clipped scale-factor ratio raised to the ILG exponent. Workers on infra-luminous gravity corrections or CPM coercivity bounds cite it when normalizing to the reference wavenumber. The definition is realized by direct algebraic substitution of the general kernel formula with k fixed at one.
claimFor a parameter bundle $P$ holding exponent $α$, amplitude $C$, and reference timescale $τ_0 > 0$, the reference-wavenumber kernel is $1 + C · (max(0.01, a / τ_0))^α$.
background
The ILG kernel is $w(k,a) = 1 + C · (a / (k τ_0))^α$, where $α = (1 - 1/φ)/2$ is derived from self-similarity and $C$ measures coercivity slack. KernelParams bundles $α$, $C$, and $τ_0$ together with the required positivity and nonnegativity conditions on those fields. This module formalizes the kernel for CPM constants derivation, reducing to unity at the reference scale $a = k τ_0$. Upstream, $τ_0$ is the fundamental tick duration from Constants and $α$ is imported from the Alpha module.
proof idea
Direct definition that substitutes the reference wavenumber k=1 into the general ILG kernel expression, applying a lower clip of 0.01 to the ratio to avoid numerical issues at small scales.
why it matters in Recognition Science
This definition supplies the reference case needed by the sibling lemma kernelAtRefK_eq to equate it to the general kernel at k=1. It anchors the ILG formalization inside the Recognition Science framework, where the exponent traces to the self-similar fixed point and the eight-tick octave. It supports the monotonicity and positivity results that follow in the same module.
scope and limits
- Does not compute the kernel for wavenumbers other than the reference value.
- Does not verify positivity or monotonicity of the result.
- Does not incorporate the full Recognition Science forcing chain beyond the supplied parameters.
formal statement (Lean)
83noncomputable def kernelAtRefK (P : KernelParams) (a : ℝ) : ℝ :=
proof body
Definition body.
84 1 + P.C * (max 0.01 (a / P.tau0)) ^ P.alpha
85