pith. machine review for the scientific record. sign in
def definition def or abbrev high

energyGap

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

Lean usage

def functionals : Functionals N := { energyGap := energyGap, .. }

formal statement (Lean)

  80noncomputable def energyGap (s : ILGState) : ℝ :=

proof body

Definition body.

  81  s.energy
  82
  83/-- Test functional: supremum over local tests (for aggregation theorem).
  84    In the gravitational context, this represents local curvature bounds. -/

used by (23)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.