Encyclopedia Cosmology Cosmology Cosmic Microwave Background From Rs Baryon Rung

ARTICLE 5 claims 3 theorems 2 models

Cosmology Cosmic Microwave Background From Rs Baryon Rung

The cosmic microwave background's first acoustic peak is measured at 220; a framework-internal number called the baryon rung is defined as 44, and 44 times 5 equals 220 exactly.

The baryon rung

The cosmic microwave background, the oldest light in the universe, carries a pattern of hot and cold spots. The angular scale of the first and largest peak in that pattern, called the first acoustic peak, tells cosmologists about the geometry and contents of the early universe. The Planck satellite measured that peak at a multipole moment of ℓ₁ = 220, with an uncertainty of about 0.5. That number is a standard observational fact, not a theoretical prediction.

In Recognition Science, a framework that derives physical structure from a single forced cost function, a small definitional object appears in this context: baryonRung, a discrete ledger entry, a named step in the framework's internal counting, is defined as the natural number 44. Another definition, configDim, a configuration dimension, is set to 5. The framework then defines the first peak as their product, and a machine-checked theorem proves that 44 times 5 equals 220. A second theorem proves that this computed 220 equals the Planck value 220. The framework also defines a second peak ratio as 507/220, about 2.305, and proves that this lies between 2.3 and 2.4, matching the observed range for the ratio of the second to the first peak.

The arithmetic is exact and machine-checked: the product 44 × 5 = 220 is a proved theorem in the framework's library, and the equality with the Planck value is also proved. But the definitions of 44 and 5 are choices, not derivations. The framework does not derive the baryon rung from its deeper principles; it sets it as a definition. The match with the measured peak is therefore an empirical observation, not a forced consequence. The framework's own documentation notes that a naive product involving the golden ratio gives about 308, not 220, and that 220 is close to 44 × 5 = 220 exactly, but the choice of 44 and 5 is not itself derived.

What the declaration establishes is narrow: a specific integer, a product, and two arithmetic equalities. It does not establish that the cosmic microwave background must have its first peak at 220, nor that the baryon rung has any physical meaning outside the framework's definitions. The agreement with Planck is real but it is a coincidence or a tuned identification, not a prediction with a falsifier. The framework's larger claims about cosmology remain open; this declaration is a small, exact piece of arithmetic attached to a measured number.

MODEL baryonRung · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
def baryonRung : ℕ := 44
MODEL configDim · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
THEOREM firstPeak_eq · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
theorem firstPeak_eq : firstPeak = 220 := by decide
THEOREM firstPeak_matches_planck · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
theorem firstPeak_matches_planck : firstPeak = firstPeakPlanck := by decide
THEOREM secondPeakRatio_band · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
theorem secondPeakRatio_band : (2.3 : ℝ) < (secondPeakRatio : ℝ) ∧ (secondPeakRatio : ℝ) < 2.4 := by
  unfold secondPeakRatio
  constructor <;> norm_num

What this page does not claim

The baryon rung is not derived from the framework's cost function; it is a definition. The match with the Planck value is not claimed to be a prediction with a named falsifier. The framework does not claim to explain why the first acoustic peak is at 220 rather than some other number.

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