Gravity Ilgderivation

The ILG time-kernel

The ILG time-kernel is a function that modifies Newtonian gravity at large scales. In Recognition Science, it is the unique correction forced by the recognition lag, the fixed cost of recognizing a later state of a system. The kernel is written w_t and it multiplies the Newtonian squared velocity. Its formula is not fitted: it is determined by two constants that come out of the forcing chain, the recognition lag C_lag = phi^-5 and the fine-structure exponent alpha = (1 - 1/phi)/2. The theorem w_t_formula_grounded states this exactly.

The kernel has two established properties that together carry the structural content of flat rotation curves. First, on the un-clamped region where the dynamical time is large enough, the kernel is strictly increasing in the dynamical time whenever alpha and C_lag are positive. Longer orbits get a strictly larger recognition-lag enhancement, so the ILG rotation curve decays strictly slower than the Keplerian curve at every radius. This is the theorem w_t_strictMono_unclamped. Second, the enhancement is unbounded: as the dynamical time grows without bound, w_t tends to infinity. No finite radius exhausts the recognition-lag correction. This is the theorem w_t_tendsto_atTop. The combined theorem rotational_flatness_forced states both properties together, and rotational_flatness_unbounded makes the divergence explicit: for any finite bound M there is a dynamical time beyond which the kernel exceeds M.

The consequence is that the enhanced squared velocity w_t(Tdyn(r)) times v_N(r)^2 decays strictly slower than the Newtonian v_N(r)^2 proportional to 1/r at every scale. That is what "rotation curves flatten" means structurally. The exact asymptotic velocity value is an empirical matter, to be settled by fits to SPARC data, not a theorem. The module does not claim a specific flat velocity; it claims the shape of the correction and its unbounded growth.

THEOREM w_t_formula_grounded · IndisputableMonolith/Gravity/ILGDerivation.lean

THEOREM w_t_strictMono_unclamped · IndisputableMonolith/Gravity/ILGDerivation.lean

THEOREM w_t_tendsto_atTop · IndisputableMonolith/Gravity/ILGDerivation.lean

THEOREM rotational_flatness_forced · IndisputableMonolith/Gravity/ILGDerivation.lean

What this page does not claim

The exact asymptotic rotation velocity is not derived here; it is an empirical matter. The fine-structure constant alpha is not derived in this module; it is an input parameter. This module does not claim a specific modified-gravity action or field equation.

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/ILGDerivation.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: