planck_l_1
plain-language theorem explainer
planck_l_1 supplies the Planck 2018 central value for the first CMB acoustic peak multipole as 220.0. Researchers comparing Recognition Science wavenumber predictions to angular data cite it when forming observed ratios such as ℓ₂/ℓ₁. The declaration is a direct constant assignment with no reduction steps.
Claim. The Planck 2018 first acoustic peak multipole satisfies $ℓ_1 = 220.0$.
background
The module develops CMB acoustic peak structure from the 8-tick lattice in StructureFormationFromBIT, deriving φ-rational wavenumber ratios k₂/k₁ = φ and k₃/k₁ = φ² at the k-level. Observed multipoles ℓ incorporate projection geometry through the angular diameter distance, so bare ℓ ratios do not equal the k-ratios. This definition supplies the empirical anchor ℓ₁ = 220.0 drawn from Planck 2018 data for ratio comparisons.
proof idea
The declaration is a direct constant definition that assigns the real number 220.0.
why it matters
It is used by planck_ratio_2_1 and planck_ratio_2_1_value to compute and bound the observed angular ratio ℓ₂/ℓ₁ ≈ 2.456. The module contrasts this value against the theorem-level φ-rational k-ratios to isolate the projection-geometry hypothesis for later transfer-function work. The constant therefore supports the framework distinction between T7 eight-tick octave predictions and observational tests in the cosmology track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.