ilg_c_matches_cpm
plain-language theorem explainer
The theorem equates the numerical coercivity bound 49/162 to the value of c_min computed from the ILG-specific constants. Researchers instantiating the CPM framework for infra-luminous gravity would cite the equality to confirm that eight-tick geometry produces a valid coercivity constant. The proof reduces to a single rewrite that invokes the precomputed value of cmin for those constants.
Claim. $49/162 = c_{min}(C)$ where $C$ denotes the ILG constants with $K_{net}=(9/7)^2$, $C_{proj}=2$, $C_{eng}=1$, and $c_{min}(C) := 1/(K_{net} C_{proj} C_{eng})$.
background
The CPM framework supplies an abstract coercivity constant defined by $c_{min}(C) = 1/(K_{net} C_{proj} C_{eng})$ for any set of positive constants $C$. The ILG module fixes these constants from eight-tick geometry: $K_{net}$ is the covering number $(9/7)^2$ arising from an $1/8$ covering radius, $C_{proj}$ equals 2 from the normalization $J''(1)=1$, and $C_{eng}$ equals 1 by energy scaling. An upstream theorem already computes the numerical value of $c_{min}$ on these constants as exactly $49/162$. The local setting is the CPM instantiation for ILG, which also records the model, coercivity theorem, and falsifiability bounds.
proof idea
The proof is a one-line wrapper that rewrites the left-hand side by the theorem ilg_cmin_value. That prior result applies simp to unfold the definition of cmin on ilgConstants followed by norm_num to obtain the rational equality.
why it matters
The equality closes the verification that the eight-tick coercivity constant matches the CPM prediction, completing one of the three main results listed in the module documentation. It supports the subsequent coercivity theorem for the ILG model and ties the T7 eight-tick octave directly to the abstract coercivity law. No open questions are addressed; the result is a direct consistency check within the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.