module module moderate

`IndisputableMonolith.Physics.StellarEvolution`

The StellarEvolution module defines nuclear efficiency for hydrogen fusion along with Gamow energy, virial temperature, and scaling relations for radius and luminosity in the Recognition Science framework. Astrophysicists applying J-cost minimization to stellar models cite these when deriving main-sequence properties from mass defect and tunneling. The module consists of definitions and short lemmas that establish constants without complex proof steps.

claimNuclear efficiency is the rest-mass fraction converted to energy in $4p → ^4$He, given by $1 - m_{^4He}/(4m_p) ≈ 0.007$. Related quantities include Gamow energy for tunneling, virial temperature from gravitational balance, and sublinear radius and luminosity scalings with mass.

background

The module sits in the Physics domain and imports JcostCore to access the J-cost function for cost-based derivations of physical parameters. It introduces nuclear_efficiency as the fractional energy release from the mass defect in proton fusion, gamow_energy for barrier penetration, virial_temperature for equilibrium, and scaling laws such as main_sequence_radius and luminosity_increases. The setting links stellar structure to the Recognition Composition Law and phi-ladder mass formulas from upstream cost definitions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies nuclear efficiency and stellar scaling relations that support larger Recognition Science results on energy production and structure. It connects to framework elements including the phi-ladder for mass formulas and constants calibrated near observed solar values. No direct parent theorems appear in the current dependency graph, but the definitions close the interface between J-cost and astrophysical observables.

scope and limits

Does not derive full stellar structure differential equations.
Does not simulate post-main-sequence evolution phases.
Does not incorporate general-relativistic corrections for compact objects.
Does not compute numerical values beyond the supplied analytic scalings.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (21)

def nuclear_efficiency L30
theorem nuclear_efficiency_valid L33
def gamow_energy L40
theorem gamow_energy_increases_with_T L45
def virial_temperature L56
theorem temp_increases_with_mass L60
def main_sequence_radius L68
theorem radius_sublinear L71
def luminosity_scaling L81
theorem luminosity_increases L84
theorem solar_calibration L90
theorem massive_star_more_luminous L95
def ms_lifetime L106
theorem lifetime_decreases L110
theorem solar_lifetime_approx L135
def chandrasekhar_limit L143
theorem endpoint_classification L146
structure MainSequenceStar L154
def ms_luminosity L158
def ms_temperature L159
theorem hr_diagram_direction L162