pith. sign in
def

firstPeak

definition
show as:
module
IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
domain
Cosmology
line
31 · github
papers citing
none yet

plain-language theorem explainer

This definition sets the first CMB acoustic peak multipole ℓ₁ to the product of the baryon rung and configuration dimension, producing exactly 220. Cosmologists matching Recognition Science predictions to Planck data would cite it to anchor the acoustic scale. It is realized as a direct arithmetic product of two upstream natural-number constants.

Claim. The first acoustic peak multipole is defined by $ℓ_1 = n_b × D_c$, where $n_b = 44$ is the baryon rung and $D_c = 5$ is the configuration dimension, so that $ℓ_1 = 220$.

background

In the Recognition Science cosmology module the cosmic microwave background acoustic peaks are obtained from the phi-ladder. The baryon rung is fixed at 44 by the mass formula on the phi-ladder in the baryon-asymmetry module. The configuration dimension is defined as D + 2 where D = 3 spatial dimensions, yielding the value 5; this count appears in both the integration-gap and coalition-size modules.

proof idea

The definition is a direct product of the baryon rung constant 44 and the configuration dimension constant 5.

why it matters

This definition supplies the numerical value certified in CMBCert to equal the Planck measurement 220 and to lie inside the observed band. It realizes the D = 3 spatial dimensions from the forcing chain (T8) together with the eight-tick octave structure, closing the link between the phi-ladder rung count and the observed first acoustic peak. It is the immediate input to the equality theorems firstPeak_eq and firstPeak_matches_planck.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.