kernel_ge_one
plain-language theorem explainer
The ILG kernel w(k, a) = 1 + C (a / (k τ₀))^α is bounded from below by 1 for all real k and a. Researchers deriving falsifiable bounds on dark matter in the Recognition Science framework cite this result to close the coercivity argument in CPMInstance. The proof unfolds the kernel definition, verifies nonnegativity of the correction term using Real.rpow_nonneg and mul_nonneg, and finishes with linarith.
Claim. For any ILG kernel parameters P (with nonnegative amplitude C and positive reference timescale τ₀), and all real wavenumbers k and scale factors a, the kernel function satisfies $1 ≤ 1 + C · (max(0.01, a / (k τ₀)) )^α$.
background
The ILG kernel is defined as w(k, a) = 1 + C · (a / (k τ₀))^α with a safeguard max(0.01, ·) to avoid division by zero when k τ₀ vanishes. KernelParams bundles the exponent α = (1 - 1/φ)/2, amplitude C ≥ 0, and reference time τ₀ > 0. Upstream, τ₀ is the fundamental tick duration from IndisputableMonolith.Constants.tau0, while the kernel definition itself appears in the same module.
proof idea
The proof unfolds the kernel definition to expose the correction term. It establishes positivity of the max argument via lt_max_of_lt_left and norm_num, nonnegativity of the power via Real.rpow_nonneg, and nonnegativity of the product via mul_nonneg. The inequality then follows immediately by linarith.
why it matters
This bound is invoked directly by ilg_falsifiable_bound to establish that the ILG kernel provides a falsifiable upper bound on dark matter effects. It closes the positivity requirement for the kernel in the ILG formalization, supporting the connection to CPM coercivity constants in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.