ilgModel
plain-language theorem explainer
ilgModel supplies the concrete CPM.Model record for the ILG gravitational modification once the energy-control hypothesis is assumed. A researcher studying coercive variational principles in modified gravity cites this construction to obtain the coercivity constant 49/162 and the associated defect bounds without re-proving the abstract framework. The definition proceeds by direct field assignment of the ILG constants together with three short algebraic verifications that the projection, energy, and dispersion inequalities hold under the given 1
Claim. Given kernel parameters $P$ and the hypothesis that defect mass of $P$ is bounded by the energy gap for every ILG state, the ILG model is the CPM model whose constants are the ILG-specific tuple, whose defect-mass and orthogonal-mass maps are those induced by $P$, whose energy-gap and test maps are the supplied functions, and whose three coercivity inequalities hold by direct substitution together with the hypothesis.
background
The module instantiates the abstract CPM.Model structure for Infra-Luminous Gravity. ILGState is the record containing scale factor, wave number, reference time scale, baryonic mass, and total energy of a gravitational configuration. EnergyControlHypothesis asserts that defect mass is bounded above by the energy gap, encoding the physical content of the variational principle (Lax-Milgram style). Upstream, the Model structure from CPM.LawOfExistence requires strictly positive constants K_net, C_proj, C_eng together with the four maps and three inequalities. The ILG constants are taken from the eight-tick aligned derivation: K_net = (9/7)^2, C_proj = 2, C_eng = 1, yielding c_min = 49/162.
proof idea
The definition constructs the record by setting C to ilgConstants, defectMass and orthoMass to the functions of P, energyGap and tests to the supplied maps, then discharges the three required proofs by simplification, norm_num, and a short calculation that uses the hypothesis together with the fact that K_net * C_proj >= 1.
why it matters
This definition supplies the concrete instance required by the coercivity theorems ilg_coercivity and ilg_reverse_coercivity. It fills the CPM instance step in the Recognition Science chain that derives all physics from the J-functional and the eight-tick octave, allowing the ILG modification to inherit the c_min = 49/162 bound. The construction makes the energy-control assumption explicit rather than hiding it inside an unfinished proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.