nuclear_efficiency_valid
plain-language theorem explainer
Nuclear efficiency ε_H, the fraction of rest mass released as energy when hydrogen fuses to helium-4, satisfies 0 < ε_H < 1. Stellar interior modelers cite the bound when closing the energy equation for main-sequence luminosity and lifetime calculations. The proof is a direct numerical normalization of the constant definition.
Claim. $0 < ε_H < 1$, where $ε_H = 0.007$ is the nuclear efficiency obtained from the helium-4 binding energy.
background
In the Recognition Science account of stellar evolution the nuclear efficiency ε_H enters the energy-generation rate for the proton-proton chain. It is fixed by the mass defect of helium-4 formation and equals 0.007 c² in the module’s units. The surrounding development obtains the observed L ∝ M^{3.9} scaling by combining this constant with the Gamow energy window, radiative opacity, and virial temperature T_c ∝ M/R. Upstream results place nuclear densities on the φ-ladder (NucleosynthesisTiers.of) and supply the dimensionless bridge K = φ^{1/2} (Constants.K) that calibrates the forcing chain.
proof idea
The proof is a one-line term-mode wrapper that applies norm_num to the definition of nuclear efficiency, which evaluates the numerical constant and discharges the two strict inequalities.
why it matters
The result supplies the physical bound required by the nuclear-burning term in the stellar-structure equations, thereby supporting the luminosity-mass relation and main-sequence lifetime formulas derived in the same module. It closes the link between the φ-forced constants (T5–T8) and observable stellar parameters without introducing additional hypotheses. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.