recombination_temperature_K
plain-language theorem explainer
The recombination temperature is fixed at 3000 K as the temperature at which the Saha equation reaches 50 percent ionization under the Recognition Science eta. Cosmologists computing the present CMB temperature from the recombination redshift would cite this constant when forming T0 = T*/(1 + z*). The declaration is a direct numerical assignment with no lemmas or reductions required.
Claim. The recombination temperature satisfies $T^* = 3000$ K, where $T^*$ is the temperature at 50 percent ionization obtained from the Saha equation with the Recognition Science baryon-to-photon ratio.
background
The CMB Temperature module derives the present-day blackbody temperature from the recombination epoch. Recombination temperature is the temperature T* at which the Saha equation yields xe = 0.5, using the RS eta value. The module then forms T0 = T*/(1 + z*) with z* approximately 1100. Upstream, the BoltzmannDistribution.temperature definition identifies temperature as the inverse of the Lagrange multiplier beta, and the doc-comment states that kB T* approximates 0.3 eV or 3500 K before adjustment to 3000 K for detailed balance.
proof idea
This is a one-line definition that directly assigns the numerical constant 3000. No lemmas are invoked and no tactics are applied beyond the abbrev expansion itself.
why it matters
The definition supplies T* that enters rs_cmb_temperature = recombination_temperature_K / (1 + rs_recombination_redshift) and thereby produces the RS prediction of approximately 2.725 K. It is referenced by cmb_is_planck_spectrum to establish that CMB photons obey the Planck spectrum at this temperature, and by recombination_energy_approx_eV to bound the energy scale near 0.26 eV. The value closes the link between the Saha-derived ionization temperature and the observed CMB, consistent with the eight-tick octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.