ilg_falsifiable_bound
plain-language theorem explainer
The ILG kernel function stays at least one for every choice of parameters and real wavenumber-amplitude pair. Modelers of infra-luminous gravity cite the bound when verifying that the modification never turns negative. The proof is a direct one-line application of the kernel_ge_one lemma already proved in the ILG kernel module.
Claim. For any ILG kernel parameter bundle $P$ and real numbers $k,a$, the kernel satisfies $w(P,k,a)geq 1$, where $w(P,k,a)=1+Ccdotmax(0.01,a/(ktau_0))^alpha$.
background
KernelParams bundles the three RS-derived constants alpha, C and tau_0 that define the ILG kernel. The kernel itself is the explicit function w(P,k,a)=1+Ccdotmax(0.01,a/(ktau_0))^alpha, taken from the ILG.Kernel module. The surrounding CPMInstance module instantiates the abstract coercive-projection framework for infra-luminous gravity, supplying the eight-tick-aligned constants K_net=(9/7)^2, C_proj=2 and c_min=49/162.
proof idea
One-line wrapper that applies the kernel_ge_one theorem from ILG.Kernel.
why it matters
The declaration supplies the concrete lower bound required by the ILG instantiation of the CPM model. It directly supports the coercivity and model theorems listed in the module documentation and closes the positivity step needed for the falsifiable dark-matter bound stated in the declaration comment. The result sits inside the Recognition Science forcing chain at the level of the ILG kernel, where the eight-tick octave and J-cost structure already fix the form of the kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.