ilgConstants
plain-language theorem explainer
ILG supplies explicit values for the four CPM constants, fixing K_net at (9/7)^2 from the eight-tick covering factor. Coercive-projection modelers cite this instantiation when checking that the ILG kernel satisfies the abstract Law of Existence. The definition is a direct record construction whose four nonnegativity fields are settled by norm_num.
Claim. The ILG constants bundle is the record with $K_{net}=(9/7)^2$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$ together with the four nonnegativity assertions $0≤K_{net}$, $0≤C_{proj}$, $0≤C_{eng}$, $0≤C_{disp}$.
background
The Constants structure from CPM.LawOfExistence packages four real parameters Knet, Cproj, Ceng, Cdisp each accompanied by a nonnegativity proof. Upstream K_net is defined as (9/7)^2 to encode the net factor from epsilon=1/8 in the eight-tick geometry. This module specializes those parameters for the ILG gravitational modification, enabling the subsequent construction of the ILG model and the explicit evaluation of its coercivity constant.
proof idea
The declaration builds the Constants record by direct assignment of the four fields to the numerical values (9/7)^2, 2, 1, 1. Each nonnegativity obligation is discharged by a single norm_num tactic that reduces the inequality to a direct rational comparison.
why it matters
This supplies the concrete constants needed to instantiate the ILG model in the CPM framework. It is used by ilgModel, ilg_cmin_value, and ilg_c_matches_cpm to verify that the eight-tick ILG constants produce the predicted coercivity bound 49/162. The choice aligns with the T7 eight-tick octave and the covering geometry of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.