Pith. sign in
module module moderate

IndisputableMonolith.Physics.StellarEvolution

show as:
view Lean formalization →

Module collecting Recognition-Science scalings for main-sequence stars: nuclear mass-to-energy efficiency of hydrogen fusion, Gamow barrier energy, virial temperature, radius and luminosity power laws, and solar calibration. A physicist deriving stellar structure from the J-cost and phi-ladder would cite these constants and monotonicity lemmas. Most statements are definitional equalities or elementary inequalities over positive reals.

claimNuclear efficiency $\eta_{\mathrm{nuc}} \approx 0.007$ for $4p\to{}^{4}\mathrm{He}$; Gamow energy $E_G(T)$ increasing in temperature; virial temperature $T_{\mathrm{vir}}(M)$ increasing in mass; main-sequence radius $R\propto M^{\alpha}$ with $\alpha<1$; luminosity $L$ strictly increasing in mass, calibrated so the solar point matches.

background

Recognition Science fixes the cost functional $J(x)=(x+x^{-1})/2-1$ (T5) and the golden ratio $\varphi$ as the self-similar fixed point (T6). Stellar structure is treated here as a thin physics layer on top of that cost: rest-mass conversion, Coulomb barrier penetration, and hydrostatic equilibrium are written as explicit real-valued functions of mass and temperature.

The only external import beyond Mathlib is the J-cost compatibility surface, which re-exports the canonical $J$ without redefinition. No eight-tick or dimension-forcing material is used; the module stays inside classical stellar-structure scalings expressed in RS-native constants where convenient.

Sibling declarations introduce nuclear efficiency ($\Delta E/mc^2\approx0.007$ for hydrogen fusion), Gamow energy, virial temperature, sub-linear radius scaling, luminosity scaling, and a solar calibration point that anchors the mass-luminosity relation.

proof idea

The module is largely definitional. Nuclear efficiency is a numerical constant with a validity lemma checking the accepted 0.007-range. Gamow energy, virial temperature, main-sequence radius and luminosity are closed-form expressions in mass and temperature; monotonicity (energy rises with $T$, temperature and luminosity rise with mass, radius exponent sub-linear) is proved by elementary calculus or algebraic comparison on $\mathbb{R}_+$. Solar calibration is an equality fixing the solar mass-luminosity point. No deep forcing-chain argument appears.

why it matters in Recognition Science

Places classical main-sequence scalings inside the Recognition monolith so later mass-ladder or luminosity arguments can cite a single physics module rather than ad-hoc constants. Downstream use is not yet wired (no used_by edges), but the declarations are the natural feed for any stellar or nucleosynthesis layer that needs $\eta_{\mathrm{nuc}}$, Gamow penetration, or $L(M)$. Ties to the broader framework only through the shared $J$-cost import; it does not itself advance T0-T8 or the fine-structure band.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (21)