Encyclopedia Cosmology Cosmology Cosmic Microwave Background From Rs Cmbcert

ARTICLE 4 claims 1 theorem 1 measured

Cosmology Cosmic Microwave Background From Rs Cmbcert

A machine-checked certificate records that a simple product of two framework numbers equals the measured position of the first acoustic peak in the cosmic microwave background.

The CMB certificate

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. Its temperature is not perfectly uniform; it carries tiny ripples. When astronomers plot the strength of those ripples against their angular size, they see a series of peaks and troughs. The first and largest peak sits at a multipole moment of ℓ₁ = 220, a number measured by the Planck satellite with an uncertainty of about 0.5. This peak corresponds to the angular scale of the largest hot and cold patches in the early universe's sound waves.

A multipole moment here is just a way of labeling angular size: higher ℓ means smaller angles on the sky. The first peak at ℓ₁ = 220 means the dominant patches are about one degree across. This is one of the most precise measurements in cosmology, and it has been confirmed by multiple experiments. The standard cosmological model explains the peak's position through the competition between gravity, which pulls matter together, and radiation pressure, which pushes it apart, in the hot plasma of the early universe.

In Recognition Science, the framework's library contains a declaration it calls CMBCert. This is a machine-checked collection of formal statements, and CMBCert is a structure that packages four facts together. It states that the first peak equals 220, that this equals the Planck measured value, that the ratio of the second peak to the first lies between 2.3 and 2.4, and that the peak can be written as a product: 44 × 5 = 220. The number 44 is called the baryonRung and 5 is called the configDim in the framework's vocabulary.

The framework's claim is not that it has derived the peak's position from first principles. The product 44 × 5 = 220 is a definitional identification, a choice of how to label the numbers, not a derivation. What CMBCert actually establishes is the arithmetic: that 44 times 5 equals 220, that 220 lies within the measured range, and that the ratio 507/220 falls between 2.3 and 2.4. These are trivial arithmetic facts, verified by the machine checker with no axioms beyond the standard logical ones.

What CMBCert does not claim is more important than what it establishes. It does not claim that Recognition Science predicts the CMB peak from its foundational principles. It does not claim that the numbers 44 and 5 are derived from the framework's forcing chain. It does not claim that the framework explains why the peak is at 220 rather than some other value. The certificate is a record of an observed coincidence, expressed in framework vocabulary, not an explanation of that coincidence.

The practical value of CMBCert is modest but real. It gives a precise, machine-checked statement of what the framework's numbers correspond to in the measured sky. A reader can see exactly what is being asserted and what is not. The arithmetic is correct, the comparison to Planck is honest, and the absence of a derivation is explicit. That is the whole content of the certificate, and it is worth knowing because it prevents the coincidence from being mistaken for a theory.

MEASURED firstPeakPlanck · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
/-- Planck measured value 220 ± 0.5. -/
def firstPeakPlanck : ℕ := 220
MODEL CMBCert · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
structure CMBCert where
  first_peak : firstPeak = 220
  matches_planck : firstPeak = firstPeakPlanck
  second_ratio_band : (2.3 : ℝ) < (secondPeakRatio : ℝ) ∧ (secondPeakRatio : ℝ) < 2.4
  decomposition : firstPeak = baryonRung * configDim
MODEL firstPeak · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
/-- ℓ₁ = baryonRung × configDim = 220. -/
def firstPeak : ℕ := baryonRung * configDim
THEOREM firstPeak_eq · firstPeak_matches_planck · secondPeakRatio_band · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
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

Recognition Science derives the CMB peak position from its foundational principles. The numbers 44 and 5 are derived from the framework's forcing chain. The framework explains why the peak is at 220 rather than some other value.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND