Ilg Cpminstance Ilg Cmin Value

The coercivity constant

Coercivity is a standard condition in analysis: a function is coercive when its values grow at least as fast as some measure of its input, so that minimizing it cannot hide at infinity. In the Recognition Science framework, a model's defect (a measure of how far a state's kernel deviates from unity, weighted by baryonic mass) must not exceed a constant multiple of its energy gap (the state's energy value). The theorem ilg_cmin_value computes that constant for the Infra-Luminous Gravity (ILG) model, a gravitational modification built on the framework's eight-tick recognition cycle.

The result is exact: for the ILG model with its chosen constants, the coercivity constant c_min equals 49/162, approximately 0.3025. This follows from three ingredients: a covering number K_net = (9/7)², a Hermitian rank-one projection bound C_proj = 2, and an energy normalization C_eng = 1. The proof is a direct computation in the machine-checked library of formal theorems, with no free parameters. A companion theorem, ilg_c_matches_cpm, confirms that this value agrees with the abstract coercive projection framework's own cmin, so the ILG instance is not a separate ad hoc choice but a faithful instantiation.

What the number buys is a guarantee. Under the energy control hypothesis (that defect mass never exceeds energy gap), the theorem ilg_reverse_coercivity states that the energy gap is at least 49/162 times the defect mass for every state. That is a quantitative floor: it says the model cannot produce arbitrarily large defects from small energies, a stability property that any useful physical model should satisfy. The bound is tight in the sense that it is the actual value, not a loose estimate.

In Recognition Science, this constant is one link in a larger chain: the framework models gravity as an emergent recognition phenomenon, and ILG is one proposed modification. The theorem does not say ILG is correct physics. It says that if you accept the framework's definitions and the energy control hypothesis, then this particular bound holds. The falsifiable content lives elsewhere, in predictions about rotation curves, not in the algebra of the constant itself.

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

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

/-- 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]

/-- Reverse coercivity: energy gap is at least c_min times defect. -/
theorem ilg_reverse_coercivity (P : KernelParams) (h_energy : EnergyControlHypothesis P) (s : ILGState) :
    (ilgModel P h_energy).energyGap s ≥ cmin (ilgModel P h_energy).C * (ilgModel P h_energy).defectMass s :=
  (ilgModel P h_energy).energyGap_ge_cmin_mul_defect ilgConstants_pos s

What this page does not claim

The theorem does not assert that ILG is a correct description of gravity. The theorem does not derive the value 49/162 from first principles; it computes it from the model's chosen constants. The theorem does not establish that the energy control hypothesis is satisfied for any particular physical system.

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: