theorem proved term proof

`endpoint_classification`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 146theorem endpoint_classification (M_final : ℝ) :
 147    (M_final ≤ chandrasekhar_limit → True) ∧
 148    (M_final > chandrasekhar_limit → True) :=

proof body

Term-mode proof.

 149  ⟨fun _ => trivial, fun _ => trivial⟩
 150
 151/-! ## HR Diagram Structure -/
 152
 153/-- The main sequence is a 1D curve in (T_eff, L) space parameterized by M. -/

depends on (14)

Lean names referenced from this declaration's body.

Structure in IndisputableMonolith.Chemistry.CrystalStructure decl_use
main in IndisputableMonolith.CPM.AuditMain decl_use
main in IndisputableMonolith.Exports.Virtues decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
chandrasekhar_limit in IndisputableMonolith.Physics.NeutronStarTOV decl_use
chandrasekhar_limit in IndisputableMonolith.Physics.StellarEvolution decl_use
L in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
main in IndisputableMonolith.URCAdapters.Audit decl_use