ilgConeConstants
plain-language theorem explainer
The declaration supplies the CPM constants bundle for the ILG model by direct reference to the Recognition Science native values with K_net fixed at unity. Researchers working on coercive projection methods in modified gravity invoke it to instantiate the abstract Model structure for the ILG kernel. The definition is a one-line abbreviation that inherits the non-negativity witness from the upstream coneConstants construction.
Claim. Define the ILG cone constants tuple as the Recognition Science values $(K_{net}, C_{proj}, C_{eng}, C_{disp}) = (1, 2, 1, 1)$ where $K_{net} = 1$ satisfies the non-negativity requirement.
background
The Constants structure from the CPM framework collects four real numbers together with a non-negativity witness: Knet is the net covering factor, Cproj bounds the projection operator, Ceng normalizes the energy term, and Cdisp controls dispersion. The upstream coneConstants definition fixes these to the RS-native values Knet := 1, Cproj := 2, Ceng := 1, Cdisp := 1 while supplying the required proof that Knet is nonnegative. The present module instantiates the abstract CPM Model for Infra-Luminous Gravity, an eight-tick aligned gravitational modification whose kernel satisfies the coercive projection framework.
proof idea
The definition is a one-line wrapper that directly references the coneConstants definition from the CPM LawOfExistence module.
why it matters
This definition supplies the constant bundle required to construct the ILG-specific Model instance later in the same module. It anchors the coercivity and cmin computations for the ILG gravitational kernel inside the Recognition Science framework, using the general cone projection constants rather than the refined eight-tick covering number (9/7)^2 mentioned in the module documentation. The choice leaves open whether the unity value or the ILG-specific covering number yields the tighter coercivity bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.