recombination_temperature_K
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from the J-cost functional equation or phi-ladder.
- Does not implement the full Saha equation or specify the precise eta factor used.
- Does not include redshift conversion or energy-unit transformations.
- Does not claim exact numerical agreement with any observational measurement beyond the stated approximation.
Lean usage
theorem rs_cmb_temperature_def : rs_cmb_temperature = recombination_temperature_K / (1 + rs_recombination_redshift) := by unfold rs_cmb_temperature cmb_temperature recombination_temperature_K rs_recombination_redshift; norm_numformal statement (Lean)
43abbrev recombination_temperature_K : ℝ := 3000 -- Kelvin
proof body
Definition body.
44
45/-- Recombination temperature is positive. -/