ILGPrediction
plain-language theorem explainer
The ILGPrediction structure packages a rotation-curve enhancement factor with its uncertainty for the ILG model. Researchers testing modified gravity against galaxy data would cite this record when stating the kernel-derived upper limit on apparent dark-matter effects. The declaration is a direct structure definition that enforces enhancement ≤ 2 as the falsifiable bound.
Claim. A record consisting of an enhancement factor $e ∈ ℝ$, an uncertainty $u ∈ ℝ$, and the constraint $e ≤ 2$, where the bound is supplied by the ILG kernel.
background
This module instantiates the abstract CPM framework for Infra-Luminous Gravity. The ILG kernel is given by $w(k,a) = 1 + C · (max(0.01, a/(k τ₀)))^α$. Constants are fixed by the eight-tick octave: $K_{net} = (9/7)^2$, $C_{proj} = 2$, $C_{eng} = 1$, producing coercivity constant $c_{min} = 49/162$ (from MODULE_DOC). Upstream kernel definitions supply the functional form used to generate the bound.
proof idea
One-line structure definition that introduces the three fields: enhancement, uncertainty, and the proposition enhancement ≤ 2.
why it matters
It supplies the concrete prediction record required by the CPM.Model instantiation for ILG. The module demonstrates that ILG satisfies the coercive projection framework with constants derived from the Recognition Science eight-tick alignment. This closes the interface between the abstract LawOfExistence and the specific ILG kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.