ilg_falsifiable_bound
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit functional form of the kernel.
- Does not supply numerical values for specific cosmological scales.
- Does not address observational constraints on dark-matter density.
- Does not extend the bound to complex or negative arguments.
formal statement (Lean)
221theorem ilg_falsifiable_bound (P : KernelParams) (k a : ℝ) :
222 kernel P k a ≥ 1 := kernel_ge_one P k a
proof body
Term-mode proof.
223
224end ILG
225end IndisputableMonolith