tov_exceeds_chandrasekhar
plain-language theorem explainer
The TOV maximum-mass lower bound from Recognition Science exceeds the Chandrasekhar limit. Compact-object astrophysicists cite the inequality to justify why neutron stars require general-relativistic hydrostatics and a stiffer equation of state than white dwarfs. The proof is a one-line term-mode wrapper that reduces the numerical comparison of the two constants to a tautology.
Claim. The Recognition-Science lower bound on the Tolman-Oppenheimer-Volkoff maximum mass satisfies $M_ {TOV} > 1.44 M_ {Ch}$, where $M_{Ch}$ is the Chandrasekhar limit for white dwarfs.
background
The NeutronStarTOV module obtains the Tolman-Oppenheimer-Volkoff equation as the J-cost minimization condition for a self-gravitating fluid. The constant chandrasekhar_limit is defined as 1.44 solar masses, the maximum mass of a white dwarf supported by electron degeneracy pressure. The abbrev rs_mass_range_low sets the Recognition-Science neutron-star mass floor at 2.0 solar masses, consistent with the observed pulsars PSR J0740+6620 and PSR J0952-0607. The upstream StellarEvolution module supplies the identical Chandrasekhar value in the context of stellar endpoints.
proof idea
The proof is a one-line term-mode wrapper that applies norm_num to the definitions of chandrasekhar_limit and rs_mass_range_low, confirming the strict inequality by direct arithmetic reduction.
why it matters
The result is invoked verbatim by the downstream theorem neutron_star_requires_stronger_eos, which concludes that neutron stars demand a stronger equation of state than white dwarfs. It supplies one of the structural bounds listed in the module documentation and aligns with the Recognition Science mass-ladder construction on the phi-ladder. The inequality closes the gap between the white-dwarf and neutron-star regimes within the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.