pith. machine review for the scientific record. sign in
structure definition def or abbrev high

ILGPrediction

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 212structure ILGPrediction where
 213  /-- Predicted rotation curve enhancement factor -/
 214  enhancement : ℝ
 215  /-- Uncertainty bound -/
 216  uncertainty : ℝ
 217  /-- The enhancement is bounded by the kernel -/
 218  enhancement_bounded : enhancement ≤ 2
 219
 220/-- The ILG kernel provides a falsifiable upper bound on dark matter effects. -/

depends on (7)

Lean names referenced from this declaration's body.