Ilg Cpminstance

The coercive bound

In physics, a coercivity condition is a guarantee that a quantity cannot become arbitrarily small while another quantity grows. Think of it as a floor under the cost: if a model is wrong, it must pay a price, and the price cannot be negotiated down to zero. The CPM (coercive projection model) framework in Recognition Science formalizes this idea for physical theories, and the module ilg cpminstance applies it to a specific modified gravity model called ILG, short for Infra-Luminous Gravity.

The ILG model modifies gravity to explain galaxy rotation curves without dark matter. Its central quantity is the defect mass, a measure of how much the model's prediction deviates from a baseline. The module proves a concrete bound: for any state of the ILG system, the defect mass is at most a constant times the energy gap, and the energy gap is at least a constant times the defect mass. The first inequality, ilg_coercivity, says the defect cannot outrun the energy; the second, ilg_reverse_coercivity, says the energy cannot ignore the defect. Together they pin the two quantities to each other.

The constants in these bounds are not free parameters. The module computes them from the eight-tick aligned ILG setup: a covering number K_net = (9/7)², a projection bound C_proj = 2, and an energy normalization C_eng = 1. These combine into the coercivity constant c_min = 49/162, and the module proves this value exactly. A separate theorem, ilg_falsifiable_bound, states that the kernel is always at least 1, which means the model's predictions stay bounded away from a trivial zero.

What this establishes in plain language: the ILG model is not a free-floating speculation. It satisfies the same structural requirement that the framework demands of any physical theory, and the requirement is checked by a machine. The module also defines a prediction structure with an enhancement factor bounded by 2, giving a concrete, testable output for rotation curves. The framework's role here is to supply the coercive projection template; the ILG module fills it in with specific numbers and proves the bounds hold.

The practical consequence is a falsifiable target. If observations of galaxy rotation curves ever require an enhancement factor above 2, the ILG model as stated here is ruled out. The module does not prove that ILG matches any particular galaxy data; it proves the model is well-formed enough to be tested at all.

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

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

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

/-- The ILG kernel provides a falsifiable upper bound on dark matter effects. -/
theorem ilg_falsifiable_bound (P : KernelParams) (k a : ℝ) :
    kernel P k a ≥ 1 := kernel_ge_one P k a

What this page does not claim

This module does not prove that ILG matches any observed galaxy rotation curve. This module does not derive the ILG model from first principles; it instantiates a pre-existing framework. This module does not address whether dark matter exists; it only bounds a modified gravity model's internal consistency.

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: