Pith. sign in
module module high

IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS

show as:
view Lean formalization →

This module assembles definitions to derive the first CMB acoustic peak multipole from Recognition Science parameters. Cosmologists testing RS-derived models against Planck data would cite the relation yielding 220. It is a definition module with no proofs that composes baryonRung and configDim.

claim$\ell_1 = \text{baryon rung} \times \text{configuration dimension} = 220$

background

The module belongs to the Cosmology domain and imports the Constants module. That upstream module defines the fundamental RS time quantum as $\tau_0 = 1$ tick.

It introduces sibling definitions including baryonRung, configDim, firstPeak, secondPeakRatio, and CMBCert. These together produce acoustic peak positions and a certification object for Planck comparison.

The local setting is the direct extraction of standard cosmological observables from the J-function and phi-ladder of Recognition Science.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the CMB peak predictions that feed higher-level cosmology claims in the Recognition Science framework. It realizes the observable consequence of the forcing chain steps T7 (eight-tick octave) and T8 (D = 3) by fixing the first peak at 220, consistent with the alpha band and mass ladder.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)