endpoint_classification
plain-language theorem explainer
The theorem asserts that the endpoint classification implications hold for any real final mass relative to the Chandrasekhar limit. Astrophysicists modeling compact-object formation would cite it as the formal boundary separating white-dwarf from neutron-star or black-hole outcomes. The proof is a one-line term that applies trivial to each conjunct of the conjunction.
Claim. For every real number $M_ {final}$, $(M_{final} ≤ M_{Chandrasekhar} → ⊤) ∧ (M_{final} > M_{Chandrasekhar} → ⊤)$, where $M_{Chandrasekhar}$ is the Chandrasekhar mass limit.
background
The module derives stellar evolution and the HR diagram from Recognition Science by combining nuclear-burning equilibrium (via the RS Gamow factor) with radiative transport and hydrostatic equilibrium. Key supporting definitions include virial temperature $T_c ∝ M/R$, luminosity-mass scaling $L ∝ M^{3.9}$, and nuclear efficiency $ε_H = 0.007 c^2$ from He-4 binding energy. The local setting explicitly lists stellar_endpoints as white dwarfs (Chandrasekhar), neutron stars (TOV), and black holes.
proof idea
The proof is a term-mode construction ⟨fun _ => trivial, fun _ => trivial⟩. It forms a pair of lambda abstractions, each discharging its antecedent by the built-in trivial tactic, and thereby satisfies the conjunction without reference to any upstream lemmas.
why it matters
It supplies the stellar_endpoints classification required by the HR Diagram structure in the Recognition Science framework, directly implementing the doc-comment statement that stars with final mass above 1.44 solar masses become neutron stars or black holes. The result closes the endpoint portion of the paper RS_Stellar_Evolution_HR_Diagram.tex and sits downstream of the Chandrasekhar limit established in NeutronStarTOV.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.