pith. sign in
module module high

IndisputableMonolith.Gravity.ILG

show as:
view Lean formalization →

The Gravity.ILG module defines the time-kernel w_t and weight functions for Information-Limited Gravity. It establishes the reference identity w_t(τ0, τ0) = 1 under nonzero tick. Derivations of modified gravity from recognition lag cite this module for the kernel definition. The module consists of definitions, parameter configurations, and supporting data structures with no embedded proofs.

claimThe time-kernel satisfies the reference identity $w_t(τ_0, τ_0) = 1$ for nonzero tick $τ_0$.

background

The module operates in the Recognition Science gravity setting and introduces the Information-Limited Gravity (ILG) time-kernel w_t together with weight functions. It supplies configuration objects (Config, Params) and derived quantities such as vbar_with, gbar_with, and w_t_with for velocity and weight calculations. The time-kernel ratio is treated as dimensionless and invariant under common rescaling.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core time-kernel definitions that the Gravity facade re-exports alongside Rotation and DerivedFactors. It directly supports the ILG Time-Kernel Derivation theorem that w_t is uniquely determined by the recognition lag C_lag = ϕ^{-5} and the fine-structure exponent α. It also underpins the spatial-kernel amplitude C = ϕ^{-2} and the rotation-curve identities in RotationILG.

scope and limits

used by (6)

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

declarations in this module (22)