ilg_is_falsifiable
plain-language theorem explainer
ILG gravity is observationally falsifiable: its kernel never falls below one, and the coercivity constant is fixed at 49/162. Cosmologists and RS auditors cite this certificate that Infra-Luminous Gravity yields concrete, testable deviations from GR. The proof is a term-mode pairing of the kernel lower bound with the arithmetic evaluation of c_min.
Claim. The Infra-Luminous Gravity kernel satisfies $w(P,k,a)\ge 1$ for every kernel parameter set $P$ and all real wavenumbers $k$ and scale factors $a$, and the coercivity constant built from the ILG CPM constants equals $49/162$.
background
This module certifies coercivity for Infra-Luminous Gravity (ILG), the RS modification of gravity whose kernel $w(k,a)=1+C\cdot(a/(k\tau_0))^\alpha$ enhances gravitational dynamics at large scales rather than suppressing them. The module frames that kernel factor, together with a fixed coercivity constant, as the source of observationally testable deviations from GR.
Coercivity is controlled by $c_{\min}=(K_{\mathrm{net}}\cdot C_{\mathrm{proj}}\cdot C_{\mathrm{eng}})^{-1}$. ILG constants come from eight-tick geometry: $K_{\mathrm{net}}=(9/7)^2$ from an $\varepsilon=1/8$ covering, $C_{\mathrm{proj}}=2$ from the $J''(1)=1$ normalization, and $C_{\mathrm{eng}}=1$. Their reciprocal is exactly $49/162$.
Upstream, kernel_ge_one proves the kernel is at least one for all parameters (the additive term is nonnegative), and ilg_cmin_value evaluates $c_{\min}$ by unfolding the ILG constants and arithmetic.
proof idea
One-line term proof. The goal is a conjunction, so the proof is the pair constructor applied to the two upstream theorems: the universal kernel lower bound, and the evaluation $c_{\min}=49/162$ for the ILG constants. No further tactics or rewriting.
why it matters
Inside the Recognition framework this is the explicit falsifiability certificate for ILG. The module states that the kernel $w(k,a)$ modifies gravitational dynamics and predicts specific deviations from GR that observations can confront, while $c_{\min}=49/162$ fixes the strength of the effect. The constants themselves are forced by eight-tick geometry (forcing-chain T7), so the numerical value is not a free fit parameter.
No downstream theorems currently depend on this declaration; it sits as a top-level verification export beside the sibling bound that the enhancement factor is finite above. It closes the non-circularity claim of the module: only arithmetic on the eight-tick constants and the kernel definition, with no measurement inputs and no axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.