orthoMass
plain-language theorem explainer
OrthoMass supplies the orthogonal mass functional for the ILG instance of the coercive projection model by equating it directly to the defect mass. Physicists modeling infra-luminous gravity modifications within the CPM framework cite this when verifying the projection-defect inequality. The implementation is a one-line alias to defectMass, which itself derives from the ILG kernel and phi-ladder scaling.
Claim. The orthogonal mass of an ILG configuration with kernel parameters $P$ and state $s$ is defined as the defect mass of that state: $orthoMass(P, s) := defectMass(P, s)$.
background
The ILG.CPMInstance module instantiates the abstract CPM model from LawOfExistence for infra-luminous gravity, using constants derived from Recognition Science such as K_net = (9/7)^2 and C_proj = 2. ILGState is the structure holding scale factor, wavenumber, reference time tau0, baryonicMass, and total energy of the gravitational configuration. Upstream results include the gap definition equaling 45 from Gap45.Derivation, the phi-forcing structure from PhiForcingDerived, and spectral emergence forcing SU(3) x SU(2) x U(1) content with exactly three generations.
proof idea
This definition is a one-line wrapper that applies defectMass to the kernel parameters and ILG state.
why it matters
This definition completes the Functionals structure required by the CPM Model in ClassicalBridge.Fluids.CPM2D, enabling Hypothesis bundles for ILG. It supports the eightTickModel and rsConeModel examples, which use the constants from the Recognition Science eight-tick alignment (T7) and projection constant C_proj derived from J''(1)=1. It touches the embedding of ILG into full 3D fluid simulations via the CPM coercivity bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.