module module

`IndisputableMonolith.Gravity.BTFREmergence`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.RAREmergence module_import

declarations in this module (11)

def a_obs_flat L49
def a_baryon_keplerian L52
def btfr_slope_naive L76
def btfr_slope_deep L89
theorem btfr_mass_velocity_relation L96
theorem btfr_deep_regime_exponent L153
theorem btfr_deep_regime L158
theorem btfr_constant_universal L169
def btfr_scatter_from_alpha_variation L182
structure BTFRCert L187
theorem btfr_cert L194