pith. sign in
module module high

IndisputableMonolith.Gravity.RAREmergence

show as:
view Lean formalization →

The RAREmergence module supplies the ILG weight function that parameterizes the Radial Acceleration Relation via an acceleration-dependent scaling. It defines w(a) = C (a0/a)^{α/2} with α near 0.191 from the RS time-acceleration bridge. Workers deriving BTFR power laws from modified gravity would cite these definitions. The module consists of definitions and direct algebraic statements with no nontrivial proofs.

claimThe ILG weight function is $w(a) = C · (a_0/a)^{α/2}$ for baryonic acceleration $a$, where $a_0$ is the characteristic scale and $α ≈ 0.191$ is the dynamical-time exponent.

background

Recognition Science places gravity modifications inside the forcing chain and J-cost framework. This module imports the fundamental time quantum τ₀ = 1 tick from Constants. The ILG weight arises from the acceleration-time bridge, with the exponent 1/2 reflecting that relation. The module introduces RAR power-law forms, log slopes, and universality statements as sibling definitions.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

These definitions feed the algebraic BTFR setup recorded in BTFREmergence, which relates ILG/RAR scaling to BTFR-style power laws. A fully structural BTFR emergence theorem with mass-independent constant remains in progress. The module supplies the mechanically checkable power-law wrappers needed for that development.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)