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
def configDim : ℕ := 5
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:
- What physical mechanism, if any, would force the baryon rung to be 44?
- How does the framework derive the configuration dimension of 5 from its deeper principles?
- Does the framework offer a derivation of the second peak ratio, or only a definition?
- What would a falsifiable prediction from the framework look like for the cosmic microwave background?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
MODEL baryonRung · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
def baryonRung : ℕ := 44The framework defines baryonRung as the natural number 44. baryonRung · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.leanMODEL configDim · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
def configDim : ℕ := 5The framework defines configDim as 5. configDim · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.leanTHEOREM firstPeak_eq · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
theorem firstPeak_eq : firstPeak = 220 := by decideA machine-checked theorem proves that 44 times 5 equals 220. firstPeak_eq · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.leanTHEOREM firstPeak_matches_planck · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
theorem firstPeak_matches_planck : firstPeak = firstPeakPlanck := by decideA second theorem proves that this computed 220 equals the Planck value 220. firstPeak_matches_planck · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.leanTHEOREM secondPeakRatio_band · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
theorem secondPeakRatio_band : (2.3 : ℝ) < (secondPeakRatio : ℝ) ∧ (secondPeakRatio : ℝ) < 2.4 := by unfold secondPeakRatio constructor <;> norm_numThe framework proves that the second peak ratio 507/220 lies between 2.3 and 2.4. secondPeakRatio_band · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean