pith. sign in
module module moderate

IndisputableMonolith.Cosmology.StructureFormationFromBIT

show as:
view Lean formalization →

Module StructureFormationFromBIT defines the phi-powered scaling for CMB acoustic peak wavenumbers as k_n = k_0 φ^n. Cosmologists modeling early structure formation on the 8-tick lattice cite these definitions to set peak positions. The module consists of targeted definitions for positions, ratios, and a certification object with no complex proofs required.

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

background

The module imports IndisputableMonolith.Constants, which defines the fundamental RS time quantum τ₀ = 1 tick. It introduces the phi-scaled wavenumber k_n = k_0 φ^n for acoustic peaks together with sibling definitions for k_peak, k_peak_pos, adjacent ratios, and scale-invariant ratios. The local setting applies the eight-tick octave to structure formation, extending the phi-ladder from the forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds IndisputableMonolith.Cosmology.CMBAcousticPeakRatios, which deepens StructureFormationFromBIT (Plan v5 Track E1) with explicit numerical-band predictions for the first three CMB acoustic-peak ratios and a falsifiable comparison to Planck 2018 data.

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)