module module moderate

`IndisputableMonolith.Physics.StellarEvolution`

This module defines stellar evolution quantities such as nuclear efficiency, Gamow energy, virial temperature, and luminosity scaling inside the Recognition Science J-cost framework. Astrophysicists deriving main-sequence relations from the phi-ladder or RCL would cite these objects. The module consists of sequential definitions and short lemmas that import JcostCore and apply its cost function to fusion and hydrostatic balance.

claim$\eta = 1 - m_{\rm He}/(4 m_p) \approx 0.007$ (nuclear efficiency); $E_G(T)$ (Gamow energy); $T_{\rm vir}(M)$ (virial temperature); $L \propto M^\alpha$ (luminosity scaling).

background

The module sits inside the Recognition Science setting supplied by the imported JcostCore, whose J-function satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Nuclear efficiency is introduced exactly as the fractional rest-mass defect in the reaction 4p → He-4. Subsequent definitions apply the same J-cost to tunneling (Gamow) and hydrostatic (virial) quantities, producing the listed sibling objects.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the nuclear-efficiency and scaling definitions that later Recognition Science stellar-structure results are expected to invoke. It directly encodes the DOC_COMMENT value of the mass defect and places it on the J-cost ladder, thereby linking T5 J-uniqueness to observable stellar parameters.

scope and limits

Does not solve the stellar structure differential equations.
Does not compute numerical evolutionary tracks.
Does not treat post-main-sequence phases.
Does not derive the mass-luminosity exponent from first principles.

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