cmb_temperature_now
plain-language theorem explainer
The declaration confirms that the CMB temperature at the present epoch equals the input value T₀ when the redshift parameter is zero. Cosmologists using Recognition Science recombination models cite this to anchor the current temperature to the observed value. The proof is a one-line wrapper that unfolds the cmb_temperature definition and simplifies the resulting expression.
Claim. For any positive real number $T_0 > 0$, the CMB temperature at redshift zero satisfies $T(T_0, 0) = T_0$, where the temperature function is defined by $T(T_*, z_*) = T_*/(1 + z_*)$.
background
The CMB temperature module derives the present-day value T₀ from the recombination epoch using the redshift scaling T = T*/(1 + z*), with T* obtained from the Saha equation at RS η and z* ≈ 1100. The upstream definition cmb_temperature implements this scaling as a direct division, and the module documentation states that the CMB is a perfect blackbody from the RS Gibbs distribution. This local setting places the result inside the chain from recombination temperature to the observed 2.725 K value.
proof idea
The proof is a one-line wrapper that unfolds the definition of cmb_temperature and applies the simp tactic to reduce the expression at z = 0 directly to the identity.
why it matters
This result anchors the current CMB temperature inside the Recognition Science framework by verifying that the redshift formula recovers the input T₀ at z = 0, closing the scaling for the present epoch as described in the module documentation. It supports the derivation T₀ = T*/(1 + z*) from the recombination temperature and redshift steps. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.