IsMaximumMass
plain-language theorem explainer
The IsMaximumMass definition marks the turnover point on the mass-central pressure curve for a TOVSolution, requiring equality at P_c_max together with a global upper bound on the mass function. Neutron star structure calculations in the Recognition Science setting would cite it to locate the stability limit where dM/dP_c changes sign. The predicate is realized directly as the conjunction of the equality and the universal inequality over all other central pressures.
Claim. For a TOV solution $sol$ with mass function $M(P_c)$, the value $M_ {max}$ is the maximum mass at central pressure $P_{c,max}$ when $M(P_{c,max}) = M_{max}$ and $M(P_c) ≤ M_{max}$ for every $P_c ≠ P_{c,max}$.
background
TOVSolution is the structure carrying the two functions M_of_Pc : ℝ → ℝ (mass versus central pressure) and R_of_Pc : ℝ → ℝ (radius versus central pressure). The module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science framework by treating hydrostatic equilibrium as a J-cost minimization condition; the Newtonian hydrostatic limit is recovered at low density. Upstream results supply the coherent-assembly mass M_max(N, ρ) = ρ · V_coherence · N and the Configuration structures from InitialCondition and RecognitionForcing that encode ledger entries as positive real ratios.
proof idea
The definition is a direct conjunction: equality of the mass function at the nominated central pressure together with the statement that every other central pressure yields a mass no larger than M_max. No lemmas are applied; the predicate is assembled from the two clauses on M_of_Pc.
why it matters
The definition supplies the predicate needed to state that the maximum stable neutron-star mass occurs where the M(P_c) curve turns over, consistent with the module's key result that maximum stable mass satisfies dM/dP_c = 0. It sits inside the Recognition Science derivation of the TOV equation and connects to the phi-ladder mass formulas and the eight-tick octave, although no downstream theorems currently reference it. The construction leaves open the precise numerical evaluation of the limit from RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.