module module

`IndisputableMonolith.Astrophysics.MassToLight`

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

used by (2)

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

IndisputableMonolith.Astrophysics module_import
IndisputableMonolith.Astrophysics.ChandrasekharMassStructure module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Astrophysics.NucleosynthesisTiers module_import
IndisputableMonolith.Astrophysics.ObservabilityLimits module_import
IndisputableMonolith.Astrophysics.StellarAssembly module_import
IndisputableMonolith.Constants module_import
IndisputableMonolith.PhiSupport.Lemmas module_import

declarations in this module (14)

def J_bit L57
def ml_derived L73
theorem ml_derived_value L79
def H_ThreeStrategiesAgree L94
theorem three_strategies_agree L101
theorem phi_in_observed_range L119
theorem phi_bounds L133
theorem ml_in_observed_range L150
theorem ml_derivation_complete L160
def AllConstantsDerived L193
def H_RSZeroParameterStatus L202
theorem rs_zero_parameter_status L210
theorem ml_derivation_falsifiable L218
def ml_summary L246