ilgConstants
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the constants from the J-cost function or Recognition Composition Law.
- Does not establish the coercivity inequality for the ILG kernel.
- Does not compute defect masses or energy gaps for specific kernel parameters.
- Does not address the alpha band or G constant in RS units.
formal statement (Lean)
95noncomputable def ilgConstants : Constants := {
proof body
Definition body.
96 Knet := (9/7)^2,
97 Cproj := 2,
98 Ceng := 1,
99 Cdisp := 1,
100 Knet_nonneg := by norm_num,
101 Cproj_nonneg := by norm_num,
102 Ceng_nonneg := by norm_num,
103 Cdisp_nonneg := by norm_num
104}
105
106/-- Alternative: RS cone constants (K_net = 1). -/