ILGState
plain-language theorem explainer
ILGState encodes the minimal configuration data for an Infra-Luminous Gravity field in the CPM coercivity setting: positive scale factor, wavenumber, reference timescale tau0, nonnegative baryonic mass norm, and total energy. Modified-gravity modelers and CPM practitioners cite this structure when instantiating the abstract Model type for ILG. The declaration is a pure structure definition carrying no proof obligations and directly supplying the fields consumed by defectMass and energyGap.
Claim. An ILG configuration state consists of a scale factor $a>0$, wavenumber $k>0$, reference timescale $τ_0>0$, baryonic mass norm $m_b≥0$, and total energy $E≥0$.
background
The CPM Instance for ILG module instantiates the abstract Model from LawOfExistence for Infra-Luminous Gravity. ILGState supplies the concrete State type that the four required functionals (defectMass, orthoMass, energyGap, tests) act upon. Upstream, the Functionals structure in CPM2D defines these maps from State to ℝ, while tau0 and tau0_pos are imported from Constants as the fundamental tick duration with its positivity lemma. The module fixes eight-tick-aligned constants: K_net = (9/7)², C_proj = 2, C_eng = 1, c_min = 49/162.
proof idea
Structure definition; the five fields and five positivity constraints are introduced directly with no tactics, lemmas, or reduction steps.
why it matters
ILGState supplies the State parameter for ilgModel, which is then used by ilg_coercivity and ilg_reverse_coercivity. It thereby connects the ILG kernel to the coercive projection framework, allowing the energy-control hypothesis to bound defect mass by the product of K_net, C_proj and C_eng. The structure therefore realizes the Recognition Science claim that ILG satisfies the CPM assumptions with constants derived from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.