ilg_cmin_value
plain-language theorem explainer
The theorem establishes that the coercivity constant for the ILG gravitational model equals 49/162. Workers on the CPM framework for modified gravity cite this explicit value when verifying that ILG satisfies the abstract coercivity bound. The proof proceeds by direct simplification of the cmin definition against the ILG constants followed by numerical normalization.
Claim. For the ILG-specific constants with $K_{net} = (9/7)^2$, $C_{proj} = 2$, and $C_{eng} = 1$, the coercivity constant satisfies $c_{min} = 1/(K_{net} C_{proj} C_{eng}) = 49/162$.
background
The CPM framework defines the coercivity constant as $c_{min} = 1/(K_{net} C_{proj} C_{eng})$, where the three factors are the net covering number, the projection bound, and the energy normalization. In the ILG module these are instantiated from eight-tick geometry: $K_{net} = (9/7)^2$ arises from the covering number at scale $1/8$, $C_{proj} = 2$ follows from the second derivative $J''(1) = 1$, and $C_{eng} = 1$ is the standard normalization. The module doc states that this yields the explicit value $c_{min} = 49/162$ for the ILG instance of the abstract CPM model.
proof idea
One-line wrapper that applies simp on the definitions of cmin and ilgConstants, then normalizes the resulting rational number.
why it matters
This supplies the concrete numerical constant required by the downstream theorem ilg_c_matches_cpm, which confirms that the ILG value agrees with the general CPM prediction. It closes the explicit computation step in the eight-tick ILG instantiation of the coercive projection framework, linking the Recognition Science constants (Knet from covering, Cproj from J) to the abstract LawOfExistence definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.