module module

`IndisputableMonolith.Physics.NeutronStarTOV`

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 (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (18)

structure TOVSystem L35
def tov_rhs L44
def newtonian_rhs L48
theorem tov_newtonian_limit L53
structure TOVSolution L65
def IsMaximumMass L70
def IsDynamicallyStable L78
def ov_limit_solar_masses L88
theorem ov_limit_positive L91
theorem true_max_exceeds_ov L95
abbrev rs_mass_range_low L104
abbrev rs_mass_range_high L105
theorem rs_mass_range_valid L107
theorem psr_j0740_in_range L110
theorem psr_j0952_in_range L113
def chandrasekhar_limit L120
theorem tov_exceeds_chandrasekhar L123
theorem neutron_star_requires_stronger_eos L128