tests
plain-language theorem explainer
The tests definition supplies the local test functional for ILG states inside the CPM coercivity model. Gravitational modelers and cosmologists working on aggregation or flatness bounds cite it when they instantiate the abstract Model for infra-luminous gravity. The definition reduces directly to the defectMass computation on the supplied state.
Claim. The test functional is defined by $tests(P,s) := defectMass(P,s)$, where $P$ denotes kernel parameters and $s$ is an ILG configuration state carrying scale factor, wavenumber, reference time scale, and baryonic mass distribution.
background
The ILG.CPMInstance module adapts the abstract CPM framework to infra-luminous gravity by supplying concrete functionals and constants derived from eight-tick geometry. ILGState is the structure that records the gravitational configuration at a given scale, with components for scale factor, wavenumber, reference time, and squared baryonic mass norm. The module imports the CPM Constants bundle (Knet, Cproj, Ceng, Cdisp) and the fundamental tick time quantum from Constants.
proof idea
The definition is a one-line wrapper that returns the value of defectMass applied to the supplied KernelParams and ILGState.
why it matters
This definition completes the Functionals record required to construct the CPM Model for ILG, which then feeds ilgModel and the coercivity theorem. Downstream it supports railEnergy computations in the periodic table, the 2D fluid bridge, and cosmological statements on the flatness problem. It aligns the local test functional with the eight-tick octave and the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.