ilg_coercivity
plain-language theorem explainer
The theorem states that in the ILG instantiation of the CPM model, defect mass of any configuration is bounded above by the product of the three model constants times the energy gap. Workers on variational principles in modified gravity cite it to verify that ILG meets the abstract coercivity requirement of the Law of Existence. The proof is a one-line term that applies the general defect_le_constants_mul_energyGap theorem to the ILG model instance.
Claim. Let $P$ be kernel parameters and suppose the energy control hypothesis holds for $P$. For any ILG configuration state $s$, the defect mass in the ILG model satisfies $D(s) ≤ (K_{net} C_{proj} C_{eng}) E(s)$, where $D$ is defect mass, $E$ is the energy gap, and the three constants are those of the model.
background
The module instantiates the abstract CPM model for Infra-Luminous Gravity. The energy control hypothesis is the statement that defect mass is at most the energy gap for every state; it makes the variational principle explicit. ILGState is the structure holding scale factor, wavenumber, reference time, baryonic mass norm, and total energy of a gravitational configuration. The upstream theorem defect_le_constants_mul_energyGap supplies the general coercivity link $D ≤ (K_{net} C_{proj} C_{eng}) (E - E_0)$ obtained by combining the projection bound on orthoMass with the energy-control bound on orthoMass.
proof idea
The proof is a one-line term that applies the general defect_le_constants_mul_energyGap theorem directly to the ILG model instance (ilgModel P h_energy) at state s. No additional tactics or reductions are required; the model already carries the three constants and the energyGap field.
why it matters
This declaration shows that the ILG gravitational modification satisfies the coercive projection framework of the CPM model with the eight-tick-aligned constants K_net = (9/7)^2, C_proj = 2, C_eng = 1. It completes the second main result listed in the module documentation and supplies the concrete coercivity inequality needed before the explicit c_min computation (49/162) can be performed. The result sits downstream of the general Law of Existence coercivity theorem and upstream of any numerical verification of ILG bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.