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:
- What physical mechanism, if any, would make the CMB peak position equal to a product of two framework integers?
- How does the framework derive the values 44 and 5 from its foundational principles, if at all?
- What other CMB features, such as the damping tail or polarization peaks, does the framework address?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
MEASURED firstPeakPlanck · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
/-- Planck measured value 220 ± 0.5. -/ def firstPeakPlanck : ℕ := 220The first peak at ℓ₁ = 220 is a number measured by the Planck satellite with an uncertainty of about 0.5. firstPeakPlanck · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.leanMODEL 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 * configDimCMBCert is a structure that packages four facts together. CMBCert · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.leanMODEL firstPeak · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
/-- ℓ₁ = baryonRung × configDim = 220. -/ def firstPeak : ℕ := baryonRung * configDimThe product 44 × 5 = 220 is a definitional identification, a choice of how to label the numbers, not a derivation. firstPeak · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.leanTHEOREM firstPeak_eq · firstPeak_matches_planck · secondPeakRatio_band · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean
theorem firstPeak_eq : firstPeak = 220 := by decidetheorem firstPeak_matches_planck : firstPeak = firstPeakPlanck := by decidetheorem secondPeakRatio_band : (2.3 : ℝ) < (secondPeakRatio : ℝ) ∧ (secondPeakRatio : ℝ) < 2.4 := by unfold secondPeakRatio constructor <;> norm_numCMBCert establishes 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. firstPeak_eq · firstPeak_matches_planck · secondPeakRatio_band · IndisputableMonolith/Cosmology/CosmicMicrowaveBackgroundFromRS.lean