pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Gravity.ILGDerivation

show as:
view Lean formalization →

ILGDerivation module establishes the unique time-kernel w_t from recognition lag C_lag = phi^{-5} and fine-structure exponent alpha. Galaxy dynamics researchers cite it when modeling modified gravity in ultra-diffuse systems. The module chains RRF gradient cost through the constants module to force the kernel and its flatness consequences.

claimThe time-kernel $w_t$ is uniquely fixed by the recognition lag $C_{lag} = ϕ^{-5}$ and fine-structure exponent $α$, thereby determining the effective modified gravity term at large scales from the RRF gradient cost.

background

Recognition Science sets the fundamental time quantum τ₀ = 1 tick in the Constants module. The ILG module supplies the base definitions for the recognition functional and its gradient cost at large scales. This derivation module connects those elements to the time-kernel via the lag parameter and α.

proof idea

The module structures the argument as a sequence of grounded theorems: first the w_t formula is fixed by the lag and α, then rotational flatness is forced, and positive and nonzero vflat are derived as direct consequences.

why it matters in Recognition Science

This module supplies the time-kernel derivation required by the UltraDiffuseGalaxies analysis for both DM-rich and DM-poor galaxies. It realizes the ILG Time-Kernel Derivation theorem, bridging the recognition lag to large-scale gravity modifications in the RS framework.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)