planck_ratio_2_1_value
plain-language theorem explainer
The theorem asserts that the Planck 2018 ratio of the second to first acoustic peak multipoles satisfies 2.45 < ℓ₂/ℓ₁ < 2.46. Researchers modeling the projection from wavenumber space to angular multipoles in the Recognition Science cosmology would cite this bound. It is established by a term-mode proof that unfolds the ratio definition and applies numerical normalization to the imported constants.
Claim. $2.45 < ℓ_2 / ℓ_1 < 2.46$, where $ℓ_1 = 220.0$ and $ℓ_2 = 540.3$ are the central values of the first and second acoustic peaks reported by Planck 2018.
background
In the Recognition Science treatment of cosmology, the CMB acoustic peaks arise from the 8-tick lattice structure in StructureFormationFromBIT. The module defines planck_l_1 as the first peak multipole ℓ₁ = 220.0 and planck_l_2 as ℓ₂ = 540.3. The ratio planck_ratio_2_1 is then their quotient, representing the observed angular-multipole ratio rather than the bare wavenumber ratio k₂/k₁ which is predicted to be φ. This distinction is emphasized in the module documentation: the observed ℓ ratios differ from k ratios due to projection geometry involving the angular diameter distance. Upstream results include the definitions of these Planck values and the ratio itself, along with foundational theorems on primitive distinctions and simplicial ledgers that underpin the lattice model.
proof idea
The proof is a term-mode wrapper. It unfolds the definitions of planck_ratio_2_1, planck_l_2, and planck_l_1, then applies the refine tactic to split the conjunction and norm_num to verify the numerical inequalities directly from the constant values.
why it matters
This result supplies the concrete numerical bound used by the downstream theorem planck_ratio_not_directly_phi to demonstrate that the observed angular ratio is not equal to φ. It fills the role of providing the empirical anchor for the hypothesis that bare k-space ratios are φ-rational (from the 8-tick octave and phi-ladder in the foundation) while the projected ℓ ratios require additional geometric factors. The module positions this as part of Track E1, distinguishing theorem-level k-ratios from the hypothesis-level projection match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.