ilgConeConstants
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values from the J-functional or the phi-ladder.
- Does not verify the coercivity inequality for the ILG kernel.
- Does not connect to the mass formula or Berry creation threshold.
formal statement (Lean)
107def ilgConeConstants : Constants := RS.coneConstants
proof body
Definition body.
108
109/-! ## CPM Model Instantiation -/
110
111/-- Energy control hypothesis: the energy of a configuration bounds its defect.
112 This is the physical content of the variational principle (Lax-Milgram).
113 In ILG, this states that the gravitational energy controls the deviation
114 from the Newtonian solution. -/