IsDynamicallyStable
plain-language theorem explainer
The IsDynamicallyStable definition encodes the neutron star stability criterion inside the Recognition Science TOV framework: a solution remains stable at central pressure P_c exactly when its mass function increases strictly for all lower pressures. Astrophysicists and general relativists modeling compact objects would cite this when locating the turnover at maximum mass against the Oppenheimer-Volkoff bound. The definition is a direct one-line translation of the dM/dP_c > 0 requirement into the StrictMonoOn predicate on the M_of_Pc component.
Claim. A TOV solution $sol$ is dynamically stable at central pressure $P_c$ if the mass function $M(P)$ is strictly increasing on the interval of pressures below $P_c$.
background
The TOVSolution structure supplies mass and radius functions of central pressure for neutron star models derived from the Recognition Science framework. The module obtains the Tolman-Oppenheimer-Volkoff equation as a J-cost minimization condition and recovers Newtonian hydrostatic equilibrium in the low-density limit. The stability definition rests on the documented fact that the maximum mass occurs where dM/dP_c = 0 and that configurations above this point are dynamically unstable.
proof idea
The definition is a one-line wrapper that applies the StrictMonoOn predicate directly to the M_of_Pc function of the supplied TOVSolution on the open interval of pressures less than P_c.
why it matters
This definition supplies the stability test required to identify the maximum stable mass in the RS-derived TOV system and thereby supports the OV lower bound of 0.71 solar masses for free neutron gas. It sits inside the module that derives structural bounds from J-cost minimization and feeds the analysis of the saddle-point condition at M_max. The placement connects to the broader RS forcing chain that fixes D = 3 and the phi-ladder mass scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.