ilg_reverse_coercivity
plain-language theorem explainer
ilg_reverse_coercivity shows that under the energy control hypothesis the ILG model obeys the lower bound energy gap at least c_min times defect mass for every state. Modified-gravity researchers would cite it to confirm that ILG meets the abstract coercivity requirement of the CPM framework. The proof is a direct one-line application of the general energyGap_ge_cmin_mul_defect theorem once positivity of the ILG constants is supplied.
Claim. Let $P$ be kernel parameters and assume the energy control hypothesis holds for $P$. For any ILG configuration state $s$, the energy gap of the ILG model satisfies energyGap$(s) ≥ c_{min} · defectMass$(s), where $c_{min}$ is the coercivity constant $1/(K_{net} · C_{proj} · C_{eng})$ of that model.
background
The module instantiates the abstract CPM model for Infra-Luminous Gravity. ILGState records scale factor, wavenumber, reference time scale, baryonic mass distribution, and total energy of a gravitational field configuration. EnergyControlHypothesis asserts that defect mass is bounded above by energy gap; this encodes the physical content of the variational principle that gravitational energy controls deviation from the Newtonian solution. cmin is defined as the reciprocal of the product of the three model constants Knet, Cproj, and Ceng; for the eight-tick-aligned ILG these are fixed at (9/7)², 2, and 1 respectively, giving the explicit value 49/162. The upstream theorem energyGap_ge_cmin_mul_defect states that whenever the three constants are strictly positive, energyGap(a) ≥ cmin · defectMass(a) holds for every configuration a.
proof idea
The proof is a one-line wrapper that applies the general coercivity theorem energyGap_ge_cmin_mul_defect from CPM.LawOfExistence to the ILG model, supplying the positivity fact ilgConstants_pos for the ILG constants Knet, Cproj, and Ceng.
why it matters
The declaration verifies that the concrete ILG model satisfies the core coercivity inequality demanded by the CPM law of existence. It thereby completes one of the main results listed in the module: that ILG fits the coercive projection framework with constants taken from Recognition Science (eight-tick octave, J-function second derivative, and the derived Knet, Cproj, Ceng). No downstream theorems yet depend on it, but it supplies the concrete check that the abstract framework applies without additional hypotheses beyond the energy control assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.