Ilg Cpminstance Ilg Alpha Eq Rs

The alpha identity

The declaration ilg_alpha_eq_rs is a theorem in the framework's machine-checked library of formal theorems. It states that for any positive time parameter tau0, the alpha parameter of the Infra-Luminous Gravity (ILG) kernel equals a fixed value called alphaLock. The proof is a definitional equality: the left side unfolds to the right side by the definitions of the kernel parameters. The theorem is a formal identity, not an empirical finding.

In the ILG model, alpha is one of the kernel parameters that shape the gravitational modification. The identity pins this parameter to a constant, alphaLock, which is part of the framework's cone constants. The theorem does not say what the numerical value of alphaLock is, nor does it derive that value from the forcing chain. It only establishes that the ILG kernel's alpha is that constant, whatever it is.

The theorem is a small piece of a larger structure. It supports the claim that ILG fits the coercive projection framework, which requires specific constants. The identity is a formal consistency check within that framework. It says nothing about whether the ILG model describes real galaxies, and it does not predict any measured rotation curve. Those are separate empirical questions, not settled by this declaration.

What the declaration does not claim is just as important. It does not claim that alphaLock equals any measured physical constant, such as the fine-structure constant. It does not claim that ILG is the correct theory of gravity. It does not claim that the value of alphaLock is derived from the fundamental cost function. The theorem is a formal equality between two defined quantities, nothing more and nothing less.

/-- The ILG exponent α matches the RS-canonical value. -/
theorem ilg_alpha_eq_rs (tau0 : ℝ) (h : 0 < tau0) :
    (rsKernelParams tau0 h).alpha = alphaLock := rfl

/-- The ILG exponent α matches the RS-canonical value. -/
theorem ilg_alpha_eq_rs (tau0 : ℝ) (h : 0 < tau0) :
    (rsKernelParams tau0 h).alpha = alphaLock := rfl

What this page does not claim

The theorem does not assert that alphaLock equals any measured physical constant, such as the fine-structure constant. The theorem does not claim that the ILG model correctly describes real galactic rotation curves. The theorem does not derive the value of alphaLock from the framework's fundamental principles.

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: