Ilg Cpminstance Ilg C Matches Cpm

The coercivity constant

In the Recognition Science framework, a ledger (a discrete record of events) of recognition events must obey a forced cost function. From that cost function, the framework derives constants and models. One such model is for Infra-Luminous Gravity (ILG), a proposed modification to gravity. A key quantity in any such model is its coercivity constant, a number that bounds how much a model's "defect mass" (a measure of deviation from a baseline) can grow relative to its energy gap (the minimum energy needed to excite a state).

The declaration ilg_c_matches_cpm establishes a precise equality: the number 49/162 equals the coercivity constant for the ILG model. This is a theorem, meaning it is proved in the machine-checked library of formal theorems. The proof is a direct calculation from the model's definition, where the constants are set as follows: the covering number K_net is (9/7)², the Hermitian rank-one bound C_proj is 2, and the energy normalization C_eng is 1. The theorem confirms that the ILG model fits the abstract coercive projection framework, which guarantees that the defect mass is always bounded by a constant multiple of the energy gap.

What this theorem does not claim is just as important. It does not assert that the ILG model is a correct description of physical reality. The model's constants are choices, not derivations from the framework's core principles. The theorem does not prove that the energy control hypothesis, which is a required assumption for the model to be well-defined, actually holds. It only shows that if that hypothesis is true, then the coercivity bound is exactly 49/162. The theorem also does not make any prediction about rotation curves or other observable phenomena; that is left to a separate structure called ILGPrediction, which is not part of this result.

The practical consequence is that the ILG model is internally consistent with the framework's requirements for a stable projection. The specific value 49/162 is a mathematical fact about the model's construction, not a physical measurement. It is a checkable, fixed number that anchors the model's analytical behavior, but it leaves the model's physical validity entirely open.

/-- The eight-tick coercivity constant 49/162 matches the CPM prediction. -/
theorem ilg_c_matches_cpm : (49 : ℝ) / 162 = cmin ilgConstants := by
  rw [ilg_cmin_value]

/-- ILG-specific CPM constants derived from eight-tick geometry.
    - K_net = (9/7)² from ε = 1/8 covering
    - C_proj = 2 from J''(1) = 1 normalization
    - C_eng = 1 standard energy normalization
    - C_disp = 1 dispersion bound -/
noncomputable def ilgConstants : Constants := {
  Knet := (9/7)^2,
  Cproj := 2,
  Ceng := 1,
  Cdisp := 1,
  Knet_nonneg := by norm_num,
  Cproj_nonneg := by norm_num,
  Ceng_nonneg := by norm_num,
  Cdisp_nonneg := by norm_num
}

/-- The ILG coercivity constant is 49/162. -/
theorem ilg_cmin_value : cmin ilgConstants = 49 / 162 := by
  simp [cmin, ilgConstants]
  norm_num

/-- The coercivity theorem for ILG: energy gap controls defect mass. -/
theorem ilg_coercivity (P : KernelParams) (h_energy : EnergyControlHypothesis P) (s : ILGState) :
    (ilgModel P h_energy).defectMass s ≤
    ((ilgModel P h_energy).C.Knet * (ilgModel P h_energy).C.Cproj * (ilgModel P h_energy).C.Ceng) *
    (ilgModel P h_energy).energyGap s :=
  (ilgModel P h_energy).defect_le_constants_mul_energyGap s

What this page does not claim

The ILG model is a correct physical description of gravity. The energy control hypothesis holds for any real system. The theorem makes any prediction about observable rotation curves.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/ILG/CPMInstance.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: