Pith. sign in
module module high

IndisputableMonolith.Cosmology.StructureFormationFromBIT

show as:
view Lean formalization →

This module defines the wavenumbers of CMB acoustic peaks via k_n = k_0 φ^n in the Recognition Science cosmology setting. Researchers deriving acoustic peak ratios from the BIT and eight-tick lattice cite these definitions. The module supplies only definitions and scaling relations drawn from the phi fixed point in upstream constants.

claimThe wavenumber at the n-th CMB acoustic peak satisfies $k_n = k_0 \phi^n$.

background

The module imports the RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants and builds wavenumber scalings on the phi-ladder. Sibling definitions include k_peak, k_peak_pos, peak ratios, and the StructureFormationFromBITCert certificate. The setting is structure formation from the BIT on the eight-tick octave lattice.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds IndisputableMonolith.Cosmology.CMBAcousticPeakRatios, which deepens StructureFormationFromBIT with explicit numerical-band predictions for the first three CMB acoustic-peak ratios and a falsifiable comparison to Planck 2018 data. It supplies the phi^n scaling for Track E1 of Plan v5.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)