firstPeak_matches_planck
plain-language theorem explainer
The equality asserts that the RS-derived CMB first acoustic peak multipole equals the Planck measurement of 220. Cosmologists using Recognition Science would cite it to confirm the exact match between the lattice prediction and satellite data. The proof reduces to a direct numerical decision on two constant natural numbers.
Claim. The first acoustic peak multipole defined by baryon rung times configuration dimension equals the Planck value 220.
background
In the CMB module the first acoustic peak is introduced as the exact product of the baryon rung (44) and configuration dimension (5), which evaluates to 220. The Planck reference is recorded as the constant natural number 220. This construction follows the module statement that the RS lattice yields ℓ₁ = 44 × 5 = 220 exactly, aligning the acoustic scale with observed data.
proof idea
The proof is a one-line term that applies the decide tactic to the concrete equality of the two natural-number definitions.
why it matters
It supplies the matches_planck field inside the CMBCert structure that aggregates the first-peak equality, second-peak ratio band, and decomposition. The result anchors the RS acoustic-scale prediction to the measured value 220, consistent with the framework's derivation of three spatial dimensions from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.