ilg_enhancement_bounded
plain-language theorem explainer
The Infra-Luminous Gravity kernel never drops below one: for any kernel parameter bundle and any wavenumber and scale factor, w(k,a) ≥ 1. Gravity modifiers and RS verification authors cite this to guarantee enhancement rather than suppression. The proof is a one-line term wrapper around the kernel lower-bound lemma.
Claim. For any ILG kernel parameter bundle $P$ (exponent $\alpha$, amplitude $C$, reference time $\tau_0$) and any real wavenumber $k$ and scale factor $a$, the ILG kernel satisfies $w_P(k,a) \ge 1$, where $w_P(k,a) = 1 + C \cdot \bigl(\max(0.01,\, a/(k\tau_0))\bigr)^{\alpha}$.
background
Infra-Luminous Gravity (ILG) is the RS modification of gravity whose kernel multiplies the Newtonian response. The module certifies coercivity and positivity facts for that kernel so the modification is observationally falsifiable rather than free-form.
The kernel is defined by $w_P(k,a) = 1 + C\cdot(\max(0.01, a/(k\tau_0)))^\alpha$, with parameters bundled in KernelParams: exponent $\alpha$, amplitude $C$, and reference time $\tau_0$. The floor at $0.01$ avoids singular division when $k\tau_0 = 0$. Upstream, the kernel lower-bound lemma already proves $1 \le w_P(k,a)$ by unfolding the definition, positivity of the max, nonnegativity of the power, and nonnegativity of $C$ under the RS parameter conventions.
Physically, $w \ge 1$ means ILG enhances gravity at large scales and never suppresses it, which is the qualitative signature used to confront dark-matter-like rotation-curve residuals.
proof idea
One-line term proof: apply the upstream lemma kernel_ge_one at the same parameters $P$, $k$, and $a$. No extra arithmetic or case splits occur at this layer; all work (unfold kernel, positivity of the max floor, nonnegativity of the power and of $C$) lives in that lemma.
why it matters
This declaration is item 3 of the ILG Coercivity Certificate: the kernel is always at least 1, so ILG enhances and never suppresses. Together with the coercivity constant $c_{\min} = 49/162$, positivity of $K_{\mathrm{net}}$, $C_{\mathrm{proj}}$, $C_{\mathrm{eng}}$, and the lock $\alpha = \mathrm{alphaLock}$, it packages the kernel as a concrete, RS-derived prediction rather than a fitted dark-matter profile.
The module frames ILG as a falsifiable RS claim: $w(k,a) = 1 + C\cdot(a/(k\tau_0))^\alpha$ produces specific large-scale deviations from GR. A lower bound of 1 is the qualitative half of that claim (enhancement direction). No downstream dependents are wired yet in the graph; the certificate itself is the consumer for verification and observational comparison pipelines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.