kernelAtRefK
plain-language theorem explainer
This definition supplies the ILG kernel at reference wavenumber k=1, giving the expression 1 + C (max 0.01, a/τ₀)^α. Researchers formalizing Infra-Luminous Gravity models cite it to fix the reference scale before proving reduction and monotonicity properties. It is implemented as a direct noncomputable abbreviation of the kernel formula with k set to unity.
Claim. For a parameter bundle P with exponent α, amplitude C and reference timescale τ₀ > 0, the reference kernel is 1 + C ⋅ (max(0.01, a/τ₀))^α.
background
The module formalizes the Infra-Luminous Gravity kernel w(k,a) = 1 + C ⋅ (a/(k τ₀))^α where α = (1 - 1/φ)/2. KernelParams bundles the components α, C and τ₀ > 0 together with the required positivity and nonnegativity conditions. Upstream, Constants.tau0 supplies the fundamental time unit τ₀ (duration of one tick) in RS-native units; the same symbol appears in Compat.Constants and Derivation modules.
proof idea
Direct definition that substitutes the reference wavenumber k=1 into the general kernel expression, replacing the ratio with the max-protected term (a/τ₀) raised to α and scaling by C before adding 1. No lemmas or tactics are invoked.
why it matters
The definition is invoked by the downstream equivalence lemma kernelAtRefK_eq, which equates it to the general kernel at k=1. It supplies the simplified case required for the module's listed main results on kernel reduction to 1 at reference scale and connection to CPM coercivity constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.