kernel_perturbation_ge_one
plain-language theorem explainer
The theorem shows the ILG perturbation kernel stays at least 1 for any valid parameter bundle P and real k_min, k, a. Cosmologists formalizing infra-luminous gravity cite it to guarantee the kernel never falls below the homogeneous mode. The proof unfolds the definition, builds three nonnegativity facts with lt_max_of_lt_left and rpow_nonneg, then closes with linarith.
Claim. For any ILG parameter bundle $P$ (with $0 < tau_0$, $0 le C$, $0 le alpha$) and real numbers $k_{min}$, $k$, $a$, the perturbation kernel satisfies $1 le 1 + C left( max(0.01, a / (max(k_{min},k) tau_0)) right)^alpha$.
background
The ILG kernel takes the form $w(k,a) = 1 + C (a/(k tau_0))^alpha$ with alpha derived from self-similarity as (1-1/phi)/2. KernelParams packages alpha, C, tau0 together with the side conditions tau0_pos and C_nonneg. The module ILG.Kernel formalizes this kernel, its positivity, monotonicity in scale factor, and link to CPM coercivity constants. Upstream, tau0 is the fundamental tick duration from Constants and the BIT kernel families supply the base kernel shapes.
proof idea
Unfold kernel_perturbation. Establish positivity of the max(0.01, ...) term via lt_max_of_lt_left and norm_num. Apply Real.rpow_nonneg to obtain nonnegativity of the power. Multiply by C_nonneg to keep the correction nonnegative. linarith finishes the inequality.
why it matters
The result supplies the pert_ge_one field of causalityBoundsCert, which packages positivity, lower bound, IR boundedness and Hubble boundedness into a single certificate. It directly addresses the concern that the kernel remains bounded as k approaches zero, fixing the ceiling by the recognition horizon. In the Recognition Science setting it supports the self-similar fixed point and the eight-tick octave through the ILG exponent alpha.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.