cmb_temperature_positive
plain-language theorem explainer
The theorem establishes that the CMB temperature remains positive when the recombination temperature is positive and the redshift exceeds -1. Cosmologists deriving the observed 2.725 K blackbody from Recognition Science recombination parameters would cite this to confirm physical consistency of the redshifted temperature. The proof is a one-line wrapper that unfolds the division formula and applies the div_pos lemma together with a linarith argument for denominator positivity.
Claim. If $0 < T_*$ and $-1 < z_*$, then $0 < T_*/(1 + z_*)$.
background
The module derives the CMB temperature from the recombination epoch in Recognition Science. The defining relation is T₀ = T*/(1 + z*), where T* is obtained from the Saha equation using the RS eta parameter and z* ≈ 1100. The upstream constant K is defined as phi to the power 1/2 and serves as a dimensionless bridge ratio between scales; a second K appears as a curvature functional but is not invoked here.
proof idea
The proof is a one-line wrapper. It unfolds cmb_temperature to expose the quotient T_star / (1 + z_star), then applies the div_pos lemma to the hypothesis 0 < T_star together with a linarith proof that 1 + z_star > 0 from the assumption -1 < z_star.
why it matters
This positivity result supports the RS prediction T₀ = 3000/(1101) ≈ 2.725 K and feeds the derivation of the Planck spectrum and anisotropy peaks. It closes a basic consistency check within the module that obtains the CMB from the recombination temperature and redshift, consistent with the Recognition Composition Law and the phi-ladder construction of constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.