firstPeakPlanck
plain-language theorem explainer
The Planck-observed first acoustic peak multipole is supplied as the integer 220. Cosmologists checking Recognition Science against CMB data cite this constant to confirm that the derived firstPeak equals the measured location exactly. The declaration is a bare constant definition with no computation or proof steps.
Claim. The Planck-measured first CMB acoustic peak multipole is the natural number $220$.
background
The module treats the cosmic microwave background acoustic peaks within Recognition Science cosmology. The first peak multipole is predicted exactly as baryonRung times configDim, which evaluates to 44 times 5. The doc-comment states that this yields 220, matching the Planck measurement of 220 within 0.5. No upstream lemmas are required; the value is introduced as the observational anchor for the certification structure.
proof idea
Direct definition that assigns the constant 220.
why it matters
This constant supplies the observational target for the CMBCert structure, which asserts firstPeak equals firstPeakPlanck together with the decomposition firstPeak equals baryonRung times configDim and the second-peak ratio band. It thereby closes the comparison between the RS phi-ladder prediction and the measured CMB spectrum, confirming the exact numerical agreement claimed in the module. The declaration touches the T7 eight-tick octave and D equals 3 spatial dimensions through the underlying rung and dimension factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.