Gravity Ilg

Gravity ILG

Gravity ILG is a module in the Recognition Science library that supplies the parametric interfaces for connecting a galaxy's dynamical time to its observed rotation curve. It is a definitional scaffold, not a derivation of gravity itself. The module defines the shapes of the baryonic velocity contributions (gas, disk, bulge), a configuration of numerical regularization parameters, and a time kernel that rescales the dynamical time before it enters the baryonic velocity sum.

The central object is the time kernel w_t, a function of a dynamical time Tdyn and a reference time τ0. It is built from a power law in the ratio Tdyn/τ0, with a parameter Clag controlling the strength of the lag and a parameter α setting the exponent. The kernel is clamped below by a small positive epsilon so it stays well defined, and the module establishes three properties of it. First, when the dynamical time equals the reference time, the kernel is exactly 1 (the reference identity). Second, the kernel is invariant under jointly rescaling both times by the same positive factor (the rescaling law). Third, under the stated parameter conditions, the kernel is nonnegative and is at least 1 whenever the dynamical time is at least the reference time.

These three lemmas are machine-checked for the default configuration, and the module also establishes the configuration's epsilon_t lies between 0 and 1. The plain-language content is that the time kernel is a well-behaved rescaling device: it does not distort the ratio of times, it returns to unity at the reference point, and it never goes negative or below one when the dynamical time is at least the reference time. The module establishes the algebraic hygiene of the bridge, not the physical claim that this bridge is how gravity works. The physical recognition-to-linking bridge that would make this a derivation of gravity remains open.

THEOREM w_t_ref · IndisputableMonolith/Gravity/ILG.lean

THEOREM w_t_rescale · IndisputableMonolith/Gravity/ILG.lean

THEOREM w_t_nonneg · w_t_ge_one · IndisputableMonolith/Gravity/ILG.lean

What this page does not claim

This module does not derive gravity from recognition principles. This module does not establish the physical recognition-to-linking bridge. This module does not fit the time kernel to any observed galaxy data.

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