cmb_temperature_scales_with_redshift
plain-language theorem explainer
The declaration proves that the CMB temperature function recovers the present-day temperature T₀ when fed the redshifted value T₀(1 + z) at redshift z. Researchers deriving the current CMB temperature from recombination-era conditions would invoke this scaling identity. The proof proceeds by unfolding the definition and applying field simplification after a linear arithmetic check that the denominator is nonzero.
Claim. For real numbers $T_0 > 0$ and $z > -1$, the CMB temperature computed from initial temperature $T_0(1 + z)$ at redshift $z$ equals $T_0$.
background
The module derives the present CMB temperature T₀ ≈ 2.725 K from the recombination temperature T* ≈ 3000 K at redshift z* ≈ 1100 using the formula T₀ = T*/(1 + z*). The function cmb_temperature(T_star, z_star) is defined as T_star / (1 + z_star), which encodes the inverse scaling of photon temperature with the cosmic scale factor a = 1/(1 + z). Upstream results include the definition of this function and basic period definitions from Breath1024 and triangular numbers from Gap45, though the latter are not directly invoked here.
proof idea
The proof unfolds the definition of cmb_temperature to obtain (T₀ (1 + z)) / (1 + z) and then applies field_simp after establishing 1 + z ≠ 0 by linarith.
why it matters
This identity confirms the consistency of the redshift scaling in the CMB temperature derivation, supporting the module's claim that T₀ = T*/(1 + z*) yields the observed 2.725 K. It underpins calculations of recombination redshift and temperature in the Recognition Science framework, where the eight-tick octave and phi-ladder inform the underlying constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.