Ilg Cpminstance Ilg Falsifiable Bound

The falsifiable bound

The declaration ilg_falsifiable_bound is a theorem in the framework's machine-checked library of formal theorems. It states that for the ILG (Infra-Luminous Gravity) model, the kernel, a function of a wavenumber and a scale, is always at least 1. In plain terms, it proves a lower bound on a central quantity of the model: no matter what parameters are chosen, the kernel cannot dip below the value 1.

ILG is a proposed modification of gravity. The kernel here acts as a multiplier that adjusts the strength of gravity relative to the standard inverse-square law. A value of 1 means the modification is off, matching ordinary gravity. A value greater than 1 means gravity is enhanced, which is the effect that could explain the flat rotation curves of galaxies without invoking dark matter. The theorem ilg_falsifiable_bound proves that this enhancement is never negative and never reduces gravity below the standard level.

This bound is what makes the model falsifiable. Because the kernel has a hard floor, the model makes a definite prediction: any observed gravitational effect that requires a kernel below 1 would contradict the model. The theorem also feeds into a broader coercivity result, which shows that the energy gap of the system is bounded below by a positive constant times the defect mass. That constant, c_min, is explicitly computed as 49/162 for this model, a number that comes from the framework's constants rather than being fitted to data.

In Recognition Science, this is part of a larger story where the cost of recognition forces specific structures. The framework models physical systems as discrete ledgers of recognition events, and the cost function J(x) = (x + 1/x)/2 - 1 is proved to be the only one satisfying five plain conditions. The ILG model is an instance of this abstract framework, and the falsifiable bound is a consequence of the kernel being defined to be at least one. The theorem does not, however, prove that ILG is the correct theory of gravity, nor does it derive the value of any measured constant from first principles.

What the bound changes is the status of the model. Before this theorem, ILG was a proposal. After it, ILG carries a concrete, checkable prediction: the kernel never goes below one. Any future measurement that finds a kernel below one would falsify the model. This is the difference between a vague hypothesis and a testable one.

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

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

/-- The ILG model satisfies CPM assumptions when the energy control hypothesis holds.
    This makes the physical assumption explicit rather than hiding it in an unfinished proof. -/
noncomputable def ilgModel (P : KernelParams)
    (h_energy : EnergyControlHypothesis P) : Model ILGState := {
  C := ilgConstants,
  defectMass := defectMass P,
  orthoMass := orthoMass P,
  energyGap := energyGap,
  tests := tests P,
  projection_defect := by
    intro s
    -- D ≤ K_net · C_proj · O
    -- Since orthoMass = defectMass for ILG, we need K_net · C_proj ≥ 1
    simp only [defectMass, orthoMass]
    have h : ilgConstants.Knet * ilgConstants.Cproj ≥ 1 := by
      simp [ilgConstants]
      norm_num
    -- defectMass ≤ K_net * C_proj * defectMass when K_net * C_proj ≥ 1
    have hdef_nonneg : 0 ≤ defectMass P s := by
      unfold defectMass
      apply mul_nonneg
      · apply sq_nonneg
      · exact s.baryonicMass_nonneg
    calc defectMass P s
        = 1 * defectMass P s := by ring
      _ ≤ (ilgConstants.Knet * ilgConstants.Cproj) * defectMass P s := by
          apply mul_le_mul_of_nonneg_right h hdef_nonneg,
  energy_control := by
    intro s
    -- orthoMass ≤ C_eng * energyGap
    -- Since C_eng = 1 and orthoMass = defectMass, this is defectMass ≤ energyGap
    simp only [orthoMass, energyGap, defectMass]
    have hCeng : ilgConstants.Ceng = 1 := rfl
    simp only [hCeng, one_mul]
    exact h_energy s,
  dispersion := by
    intro s
    -- orthoMass ≤ C_disp * tests
    -- Since tests = defectMass = orthoMass and C_disp = 1, this is equality
    simp only [orthoMass, tests]
    have h : ilgConstants.Cdisp = 1 := rfl
    simp [h]
}

What this page does not claim

This theorem does not prove that ILG is the correct theory of gravity. This theorem does not derive the value of any measured physical constant from first principles. This theorem does not claim the kernel is exactly 1, only that it is at least 1.

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: