rs_recombination_redshift
plain-language theorem explainer
The declaration assigns the recombination redshift z* the fixed numerical value 1100. Cosmologists deriving the present-day CMB temperature from the recombination epoch would cite this constant when applying the redshift formula T0 = T*/(1 + z*). The assignment is a direct numerical binding with no lemma invocations or tactic steps.
Claim. The recombination redshift satisfies $z^* := 1100$.
background
In the CMB Temperature module the present-day temperature T0 follows from the recombination temperature T* ≈ 3000 K via T0 = T*/(1 + z*), where z* is calibrated from the Saha ionization equation using the Recognition Science baryon-to-photon ratio η together with Ω_b h² = 0.022. The module imports JcostCore and relies on empirical program structures to guarantee collision-free conditions in the underlying ledger. Upstream results supply supporting algebraic tautologies from simplicial ledgers and mechanism-design structures that keep the redshift assignment free of hidden hypotheses.
proof idea
The declaration is a direct numerical abbreviation; it binds the real number 1100 with no tactic applications or lemma calls.
why it matters
This constant supplies the redshift input to rs_cmb_temperature and the approximation theorem rs_cmb_approx_2725, which verify the RS prediction |T0 - 2.725| < 0.001 K. It bridges the recombination epoch (T* from the Saha equation) to the observed blackbody spectrum, consistent with the eight-tick octave and phi-ladder scaling. The paper RS_CMB_Temperature.tex positions the value as the link from early-universe physics to the Planck spectrum at T0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.