kernel_pos
plain-language theorem explainer
The positivity result for the ILG kernel establishes that w(k, a) = 1 + C (max(0.01, a/(k τ₀)))^α stays strictly above zero for any valid KernelParams P and all real k, a. Cosmologists and modified-gravity modelers cite it when they need to guarantee that Poisson potentials remain well-defined and sign-stable. The proof unfolds the kernel, verifies the max base is positive, applies nonnegativity of real powers and multiplication, then closes with linarith.
Claim. Let P be a KernelParams structure with nonnegative amplitude C, nonnegative exponent α, and positive reference time τ₀. For all real wave numbers k and scale factors a the kernel satisfies 0 < 1 + C (max(0.01, a/(k τ₀)))^α.
background
The ILG.Kernel module formalizes the Infra-Luminous Gravity kernel w(k, a) = 1 + C (a/(k τ₀))^α, where α = (1 - 1/φ)/2 is the self-similarity exponent and C encodes coercivity slack. KernelParams is the structure that packages α, C, and τ₀ together with the required positivity and nonnegativity proofs. Upstream, τ₀ is supplied as the fundamental tick duration from the Constants module (defined via sqrt(hbar G / (π c³))/c in the derivation) and the kernel appears in BITKernelFamilies for cosmological applications. The module setting connects directly to CPM coercivity constants as described in the supporting LaTeX document.
proof idea
The proof unfolds the kernel definition to expose 1 + C times the powered max term. It shows max(0.01, a/(k τ₀)) > 0 by lt_max_of_lt_left and norm_num. Real.rpow_nonneg then gives nonnegativity of the power, mul_nonneg (using C_nonneg) gives nonnegativity of the product, and linarith concludes strict positivity.
why it matters
This result is invoked by poisson_coercive to prove the modified potential never vanishes for nonzero sources and by poisson_enhancement to show the ILG potential equals the kernel factor times the GR potential. It discharges the first main result in the module documentation (well-defined and positive kernels). In the Recognition framework it ensures the kernel term enters the forcing chain without sign defects, supporting the ILG extension of the Poisson operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.