Gravity Rotation Ilg

The ILG rotation law

Gravity rotation ILG is the Recognition Science relation between a galaxy's rotation velocity v at radius r and the enclosed mass M(r). The relation is a fixed-point equation: v² equals the product of a dimensionless factor called the inertial link gain (the factor by which recognition cost modifies inertial response) and the Newtonian term G M(r)/r. The gain itself depends on the orbital period 2πr/v and on a time parameter τ₀.

The module proves that for any positive radius, any positive enclosed mass, and any admissible gain parameters, a positive velocity satisfying the fixed-point equation exists. This is the theorem solution_exists. The equation is not a fit to data; it is the form forced by the recognition ledger once the gain is specified. The module also names a falsifier: if the global-only fit, with mass-to-light ratio equal to the golden ratio and the locking value of the gain parameter, fails to match the SPARC database within a chi-squared per degree of freedom threshold of 2.0, the model is falsified.

The plain-language content is that the rotation curve is not an independent empirical curve but a consequence of the same cost structure that forces other Recognition Science constants. The existence theorem guarantees the equation is well-posed: it always has a positive solution, so the model never leaves a galaxy without a predicted rotation velocity. The falsifier is the honesty organ: it states exactly what measurement would kill the model.

MODEL is_ilg_vrot · IndisputableMonolith/Gravity/RotationILG.lean

THEOREM solution_exists · IndisputableMonolith/Gravity/RotationILG.lean

MODEL SPARC_mismatch_falsifier · IndisputableMonolith/Gravity/RotationILG.lean

What this page does not claim

This answer does not claim the ILG rotation law has been verified against SPARC data. This answer does not claim the inertial link gain's explicit functional form is derived in this module. This answer does not claim the golden ratio mass-to-light ratio is derived here rather than chosen.

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/Gravity/RotationILG.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: