secondPeakRatio_band
plain-language theorem explainer
The theorem confirms that the CMB second acoustic peak ratio falls strictly between 2.3 and 2.4 under the Recognition Science model. Cosmologists validating RS predictions against Planck observations cite this interval. The proof unfolds the ratio definition as 507/220 and checks the bounds via numerical tactics.
Claim. The ratio of the second to first CMB acoustic peak obeys the strict inequality $2.3 < r < 2.4$, where $r = 507/220$.
background
The module develops CMB acoustic peaks within Recognition Science by fixing the first peak multipole at exactly 220 through the product of baryon rung 44 and configuration dimension 5. The second peak ratio is introduced as the constant 507/220 to capture the observed scaling between peaks. This setup allows certification that RS predictions align with Planck data within the specified band.
proof idea
Unfolding the definition of the second peak ratio exposes the fraction 507/220. The constructor tactic splits the conjunction into two inequalities, each discharged by norm_num through direct computation on the rationals.
why it matters
It populates the second ratio band component of the cmbCert structure, which certifies the complete CMB peak decomposition against Planck values. The module documentation positions this bound as essential for confirming the RS prediction of the acoustic spectrum, including the exact first peak at 220. This closes one element of the F4 cosmology depth verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.