energyGap
plain-language theorem explainer
The declaration defines the energy gap for an ILG configuration state as its total energy field. Researchers assembling CPM models for modified gravity cite it when populating the four functionals in LawOfExistence.Model. The definition is a direct one-line field projection from the ILGState record.
Claim. For an ILG configuration state $s$, the energy gap is the total energy component $E(s)$ of the gravitational field configuration.
background
The module supplies a concrete CPM instance for Infra-Luminous Gravity that satisfies the abstract coercive projection framework. ILGState records the essential data at a given scale: scale factor, wavenumber, reference time scale, baryonic mass squared norm, and total energy. MODULE_DOC states that the eight-tick aligned constants are K_net = (9/7)^2, C_proj = 2, C_eng = 1, and c_min = 49/162. The definition depends on the meta-realization structure from UniversalForcingSelfReference.for and on the sibling tests functional.
proof idea
One-line definition that extracts the energy field directly from the ILGState record.
why it matters
This supplies the energyGap slot required by CPM.LawOfExistence.Model and is referenced by the Hypothesis bundle and model construction in ClassicalBridge.Fluids.CPM2D. It also feeds the eightTickModel and rsConeModel in CPM.Examples. The definition closes the energy-control leg of the coercivity argument for ILG, consistent with the eight-tick octave and the J-cost structure from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.