pith. sign in
module module high

IndisputableMonolith.Gravity.BTFREmergence

show as:
view Lean formalization →

The BTFREmergence module derives the Baryonic Tully-Fisher Relation as a direct consequence of the ILG weight function and the already-established RAR. It produces explicit mass-velocity scalings, regime exponents, and scatter bounds using only RS constants and the flat-rotation acceleration definition. Galaxy-dynamics researchers cite it for the algebraic link between observed centripetal acceleration and baryonic mass in the deep-MOND-like regime. The module consists of a short chain of algebraic reductions and case splits that inherit their

claimDefine observed centripetal acceleration at radius $r$ for flat rotation by $a_0(r) = v^2/r$. The module proves the BTFR mass-velocity relation $M_b = (v^4 / G) C$ together with the deep-regime exponent 4, the universal constant $C$, and scatter induced by small variations in the fine-structure parameter inside the interval $(137.030,137.039)$.

background

The module sits inside the gravity domain and imports the RS time quantum from Constants together with the full RAR emergence theorem from RAREmergence. RAR itself states that observed acceleration correlates with baryonic acceleration through the ILG weight function; the present module simply specializes that correlation to the flat-rotation case. The central definition supplied here is a_obs_flat, which extracts the centripetal acceleration $v^2/r$ once the rotation curve has become flat.

proof idea

The module is a collection of short algebraic derivations rather than a single tactic script. It begins with a_obs_flat, applies the RAR identity to obtain the naive slope, then splits into deep and shallow regimes to extract the exact exponent 4 and the universal prefactor. Scatter is obtained by differentiating with respect to the alpha interval already bounded in Constants. Each step is a one-line wrapper that substitutes the upstream RAR result.

why it matters in Recognition Science

BTFREmergence supplies the second major galactic scaling relation after RAR, completing the emergence of observed rotation-curve phenomenology from the ILG weight function. It is the direct parent of any later claim that RS reproduces the Tully-Fisher slope and its small scatter without dark-matter halos. The module therefore sits at the same level as the RAR emergence result and inherits the same claim status once the upstream RAR theorem is accepted.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)