rs_cmb_temperature
The definition computes the present-day CMB temperature as the recombination temperature divided by one plus the recombination redshift. Cosmologists working inside the Recognition Science framework cite this value when matching the predicted 2.725 K to observations. It is a direct substitution into the cmb_temperature formula using the pre-derived recombination inputs.
claim$T_0 = T^*/(1 + z^*)$ where $T^*$ is the recombination temperature in kelvin and $z^*$ is the recombination redshift.
background
The CMB Temperature module derives the present-day blackbody temperature from the recombination epoch. Recombination temperature is obtained from the Saha equation with the RS eta parameter and yields approximately 3000 K. Recombination redshift is fixed near 1100. The module states the relation T0 = T*/(1 + z*) explicitly.
proof idea
One-line definition that applies the cmb_temperature function to recombination_temperature_K and rs_recombination_redshift.
why it matters in Recognition Science
This supplies the temperature argument for the theorem that CMB photons obey the Planck spectrum and for the numerical check that the value lies within 0.001 of 2.725 K. It closes the RS derivation of T0 from recombination parameters, consistent with the phi-ladder constants and the eight-tick structure. The module references the paper RS_CMB_Temperature.tex.
scope and limits
- Does not derive recombination temperature or redshift from more primitive axioms.
- Does not treat CMB anisotropies, polarization, or late-time reionization.
- Does not incorporate curvature or lambda terms beyond the fixed K bridge.
Lean usage
theorem rs_cmb_approx_2725 : |rs_cmb_temperature - (3000 / 1101 : ℝ)| < 0.001 := by unfold rs_cmb_temperature cmb_temperature recombination_temperature_K rs_recombination_redshift; norm_numformal statement (Lean)
78noncomputable def rs_cmb_temperature : ℝ :=
proof body
Definition body.
79 cmb_temperature recombination_temperature_K rs_recombination_redshift
80
81/-- The RS prediction is approximately 2.725 K. -/