recombination_temperature_positive
plain-language theorem explainer
Recombination temperature positivity follows from its explicit definition as 3000 K in the Saha-equation model. Cosmologists deriving the present-day CMB temperature from the recombination epoch redshift would cite this result to confirm physical consistency before applying the blackbody formula. The proof is a one-line numerical verification of the constant.
Claim. The recombination temperature $T^*$ satisfies $0 < T^*$, where $T^*$ is the temperature at 50 percent ionization obtained from the Saha equation and equals 3000 K.
background
The module derives the CMB temperature $T_0 = 2.725$ K from the recombination temperature $T^$ at redshift $z^ ≈ 1100$. Recombination_temperature_K is introduced as the abbrev 3000 K, the value at which the Saha equation with RS eta yields equal ionized and neutral fractions. Upstream results supply the Boltzmann constant $k_B$ in information, quantum, and thermodynamics contexts, all using the same numerical definition.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic directly to the constant definition of recombination_temperature_K.
why it matters
This result supplies the basic positivity check required for the blackbody spectrum and anisotropy peak derivations in the CMB module. It supports the formula $T_0 = T^/(1+z^)$ and the planck spectrum claim in RS_CMB_Temperature.tex before proceeding to higher-order structure. No open questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.