defectMass
plain-language theorem explainer
Defect mass for an ILG configuration quantifies the squared deviation of the kernel value from unity, scaled by the baryonic mass distribution. Cosmologists and modified gravity theorists cite this when embedding ILG into the coercive projection model for bounding dark-matter-like effects. The definition evaluates the kernel at the state's wavenumber and scale then applies the algebraic factor (w minus one) squared.
Claim. Let $P$ be kernel parameters and $s$ an ILG state with wavenumber $k$, scale $a$, and baryonic mass $m_b$. The defect mass is $(K(P, k, a) - 1)^2 m_b$, where $K$ denotes the kernel function.
background
The ILGState structure holds the scale factor, wavenumber, reference time, and baryonic mass for a gravitational configuration in the infra-luminous gravity model. The kernel function, drawn from BIT kernel families, computes a scale-dependent modification factor. Upstream, the defect functional from the Law of Existence is defined as the J-cost, which here specializes to the squared deviation from the Newtonian limit.
proof idea
One-line wrapper that evaluates the kernel at the given wavenumber and scale, then multiplies the squared deviation from one by the baryonic mass.
why it matters
This definition supplies the defectMass component of the Functionals structure used to build the CPM Model for ILG. It feeds directly into the bridge construction in ClassicalBridge.Fluids.CPM2D and the eightTickModel example. Within Recognition Science it instantiates the defect measure for the ILG modification, consistent with the eight-tick octave and the projection onto the orthogonal complement of the Newtonian subspace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.