EnergyControlHypothesis
plain-language theorem explainer
EnergyControlHypothesis encodes the assumption that for kernel parameters P the defect mass of any ILG state is at most its energy gap. Modelers of ILG within the CPM framework cite it to isolate the variational principle as an explicit hypothesis rather than an implicit step. The declaration consists of a direct Prop definition without additional lemmas or reductions.
Claim. For kernel parameters $P$, the hypothesis asserts that for every ILG state $s$ the defect mass of $s$ under $P$ is at most the energy gap of $s$.
background
The CPMInstance module for ILG instantiates the abstract CPM model. ILGState is the structure holding scale factor, wavenumber, and reference time scale for a gravitational configuration. defectMass(P, s) is the squared L2 deviation (w-1)^2 weighted by baryonic mass, measuring departure from the Newtonian solution. energyGap(s) equals the state's excess energy above the Newtonian ground state. KernelParams bundles the RS-derived values alpha, C, and tau0.
proof idea
The declaration is a one-line definition of the Prop as the universal quantification that defectMass P s is less than or equal to energyGap s for all ILGState s. No lemmas are applied.
why it matters
It is required by the ilgModel definition and by the coercivity theorems ilg_coercivity and ilg_reverse_coercivity. These results establish that the ILG model satisfies CPM bounds with constants K_net = (9/7)^2, C_proj = 2, C_eng = 1, and c_min = 49/162 drawn from the eight-tick octave. The hypothesis makes the Lax-Milgram content explicit for the ILG instantiation of the CPM framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.