recombination_redshift_positive
plain-language theorem explainer
The declaration proves the Recognition Science recombination redshift is strictly positive. Cosmologists deriving the CMB temperature from the recombination epoch would cite this to confirm the input to T₀ = T*/(1 + z*) exceeds zero. The proof is a one-line numerical normalization on the hardcoded constant 1100.
Claim. $0 < z^*$ where $z^* = 1100$ is the recombination redshift obtained from the Saha equation with Recognition Science baryon density parameter.
background
The module computes the present CMB temperature as T₀ = T*/(1 + z*), where z* is the recombination redshift and T* the recombination temperature. The upstream definition rs_recombination_redshift supplies the constant 1100 arising from the Saha equation with RS η and Ω_b h² = 0.022. Temperature itself is defined as the inverse of the Lagrange multiplier β in the Boltzmann distribution.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the constant 1100.
why it matters
This positivity result anchors the CMB temperature formula T₀ = T*/(1 + z*) inside the Recognition Science derivation of the observed 2.725 K blackbody. It supplies the required sign check for the redshift term in the module's key results, consistent with the eight-tick octave and phi-ladder scaling used elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.