Physics Stellar Evolution

Stellar evolution as forced structure

Stellar evolution in Recognition Science is the study of how the forced cost law propagates into the life cycle of stars. The framework derives the main sequence and the Hertzsprung-Russell (HR) diagram from the same recognition ledger that forces the golden ratio and three spatial dimensions. The module StellarEvolution establishes the quantitative relations that govern a star's life: its temperature, luminosity, radius, lifetime, and final fate.

The central result is the main sequence luminosity scaling, L ∝ M^3.9. This follows from nuclear burning equilibrium, expressed through the Gamow factor, combined with radiative transport and hydrostatic equilibrium. The module defines this scaling as a function of mass and proves that it increases monotonically with mass: a more massive star is more luminous. The same structure yields the main sequence radius scaling, R ∝ M^0.8, and the virial temperature relation, T_c ∝ M/R, both established monotonic in mass. The HR diagram direction follows: a more massive main sequence star is both more luminous and hotter.

The module also establishes the nuclear efficiency of hydrogen burning, ε_H = 0.007 c², from the binding energy of helium-4. This efficiency is established to lie strictly between zero and one. The main sequence lifetime is defined as t_MS ∝ M^(-2.9), combining the efficiency with the luminosity scaling. The theorem lifetime_decreases proves that more massive stars live shorter lives. The solar calibration is exact: a star of one solar mass has luminosity one in the module's units, and its lifetime is the product of the nuclear efficiency and 0.7.

Stellar endpoints are classified by the Chandrasekhar limit of 1.44 solar masses. The module defines the limit and proves a classification theorem: final masses at or below the limit are consistent with white dwarf formation, and masses above it are consistent with neutron stars or black holes. The classification is a theorem about the ordering, not a proof that any particular star reaches any particular endpoint.

THEOREM luminosity_scaling · luminosity_increases · IndisputableMonolith/Physics/StellarEvolution.lean

THEOREM hr_diagram_direction · IndisputableMonolith/Physics/StellarEvolution.lean

THEOREM nuclear_efficiency · nuclear_efficiency_valid · IndisputableMonolith/Physics/StellarEvolution.lean

THEOREM lifetime_decreases · IndisputableMonolith/Physics/StellarEvolution.lean

THEOREM chandrasekhar_limit · endpoint_classification · IndisputableMonolith/Physics/StellarEvolution.lean

What this page does not claim

This module does not prove that any particular observed star follows the derived scaling relations. The stellar endpoint classification does not prove the physical formation mechanism for white dwarfs, neutron stars, or black holes. The nuclear efficiency value is defined from helium-4 binding energy, not derived from the recognition cost law itself.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/StellarEvolution.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: