Cosmology Cosmic Microwave Background From Rs First Peak Eq

The first acoustic peak

The cosmic microwave background (CMB) is the oldest light in the universe, a faint glow left over from about 380,000 years after the Big Bang. Imprinted on that glow are tiny temperature ripples, and those ripples form a series of peaks when plotted against angular scale. The first peak, at a multipole of ℓ₁ = 220, corresponds to the largest scale on which sound waves in the early plasma had time to compress once before the universe became transparent. The European Space Agency's Planck satellite measured this peak at 220 ± 0.5, a value confirmed across multiple experiments.

In the Recognition Science framework, the number 220 is not taken from observation; it is built from two internal constants. The framework defines a baryon rung (a discrete step in its particle ladder, set to 44) and a configuration dimension (a count of spatial degrees of freedom, set to 5). Their product, 44 × 5 = 220, is the framework's predicted first peak. The declaration firstPeak_eq is a machine-checked theorem in the framework's library of formal theorems: it proves, by direct computation, that this product equals 220 exactly. A companion theorem proves that this equals the Planck value 220, and a separate result places the ratio of the second to first peak, 507/220 ≈ 2.305, inside the observed band (2.3, 2.4).

What the declaration does not claim is just as important. It does not derive the constants 44 and 5 from first principles; those are definitional choices, not theorems. The match to Planck is a numerical coincidence verified in the formal system, not a derivation of the CMB from the framework's axioms. The framework has not yet produced a physical model that explains why the acoustic peak must sit at this multipole; the bridge from its abstract cost function to the plasma physics of the early universe remains an open target. The theorem is a precise arithmetic statement, and the agreement with measurement is exact to the integer, but the physical mechanism is not yet derived.

theorem firstPeak_eq : firstPeak = 220 := by decide

theorem firstPeak_matches_planck : firstPeak = firstPeakPlanck := by decide

theorem secondPeakRatio_band : (2.3 : ℝ) < (secondPeakRatio : ℝ) ∧ (secondPeakRatio : ℝ) < 2.4 := by
  unfold secondPeakRatio
  constructor <;> norm_num

What this page does not claim

The constants 44 and 5 are derived from first principles; they are definitional choices. The framework provides a physical derivation of the cosmic microwave background from its axioms. The match to Planck is a prediction with a falsifier; it is a verified arithmetic coincidence. The framework explains why the acoustic peaks have their observed heights or widths.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: