rs_cmb_consistent_with_firas
plain-language theorem explainer
The declaration verifies that the Recognition Science structural prediction for the cosmic microwave background temperature, computed as 3000 divided by 1101, differs from the FIRAS observed value of 2.72548 K by less than 0.01 K. Researchers in Recognition Science cosmology would reference this to demonstrate quantitative agreement between the model's recombination redshift and blackbody temperature with satellite data. The verification relies on a direct numerical computation that confirms the inequality holds.
Claim. The absolute difference satisfies $|3000/1101 - 2.72548| < 0.01$.
background
In the Recognition Science framework the CMB temperature emerges from the recombination epoch at temperature approximately 3000 K combined with redshift approximately 1100, so that the present temperature follows the division formula. The module treats the Planck spectrum as the RS Gibbs distribution for photons over the eight-tick full period and derives the recombination temperature via the Saha equation with the RS eta parameter. Upstream constants include the fundamental tick as the RS-native time quantum and period definitions that supply the structural constants entering the redshift and temperature ladder.
proof idea
The proof is a one-line wrapper that applies norm_num to evaluate the numerical inequality directly.
why it matters
This result anchors the RS prediction for the CMB temperature within observational bounds and supports the derivation from recombination temperature and redshift given in the module. It aligns with the framework's eight-tick octave that informs the photon distribution and the phi-ladder constants that fix the recombination parameters. No downstream theorems are listed, so the declaration functions as a terminal consistency check rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.