pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS

show as:
view Lean formalization →

The module sets the first CMB acoustic peak position ℓ₁ to 220 by defining it as the product baryonRung times configDim. Cosmologists comparing RS-derived spectra to Planck data would cite these definitions. The module supplies direct equalities and a certification object without algebraic reductions or tactic scripts.

claim$ℓ_1 = $ baryonRung $×$ configDim $= 220$

background

The module operates inside the Recognition Science cosmology layer and imports the base time quantum τ₀ = 1 tick from IndisputableMonolith.Constants. It introduces baryonRung as the phi-ladder rung assigned to baryonic matter and configDim as the effective dimension factor fixed by the T8 forcing step. These two quantities multiply to give the angular scale of the first acoustic peak.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the numerical value of the first acoustic peak that downstream cosmology results reference when matching RS predictions to observed CMB data. It closes the step that links the eight-tick octave and D = 3 spatial dimensions to the measured ℓ₁ ≈ 220 band.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)