ilgConstants_pos
The theorem establishes positivity of the ILG constants K_net, C_proj, and C_eng in the coercive projection model. Researchers instantiating the CPM framework for infra-luminous gravity cite it to confirm the constants meet the framework's positivity requirements before applying energy-gap bounds. The proof is a one-line term-mode reduction that simplifies the explicit definitions and checks the resulting numerical inequalities.
claim$K_{net} > 0$, $C_{proj} > 0$, and $C_{eng} > 0$, where these are the ILG constants given by $K_{net} = (9/7)^2$, $C_{proj} = 2$, and $C_{eng} = 1$.
background
The module supplies a concrete CPM.Model instance for infra-luminous gravity using constants derived from eight-tick geometry. The definition ilgConstants sets K_net to the square of the covering number for ε = 1/8, C_proj to the Hermitian rank-one bound from J''(1) = 1, and C_eng to the standard energy normalization. These values appear directly in the model construction and in the coercivity statements that follow.
proof idea
The proof is a one-line term-mode wrapper. It refines the three-way conjunction, simplifies each conjunct by unfolding the definition of ilgConstants, and applies norm_num to verify the three explicit positive rationals.
why it matters in Recognition Science
This result supplies the positivity hypothesis required by the downstream reverse-coercivity theorem ilg_reverse_coercivity, which asserts that the energy gap is at least c_min times the defect mass. It closes the constant-positivity step in the CPM instantiation for ILG and connects to the eight-tick octave and J-cost functional of Recognition Science. The parent theorem applies the positivity fact directly to obtain the coercivity bound.
scope and limits
- Does not derive the numerical values of the constants from first principles.
- Does not prove the coercivity bound or the energy-gap inequality.
- Does not address the full ILG kernel or state definitions.
- Does not extend to gravitational modifications other than ILG.
Lean usage
(ilgModel P h_energy).energyGap_ge_cmin_mul_defect ilgConstants_pos sformal statement (Lean)
183theorem ilgConstants_pos :
184 0 < ilgConstants.Knet ∧ 0 < ilgConstants.Cproj ∧ 0 < ilgConstants.Ceng := by
proof body
Term-mode proof.
185 refine ⟨?_, ?_, ?_⟩ <;> simp only [ilgConstants] <;> norm_num
186
187/-- The coercivity theorem for ILG: energy gap controls defect mass. -/