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

IndisputableMonolith.Cosmology.StructureFormationFromBIT

show as:
view Lean formalization →

This module defines the wavenumber scaling for CMB acoustic peaks as k_n = k_0 φ^n together with adjacent ratio functions and a certification theorem. Cosmologists deriving structure formation from the BIT foundation cite it to obtain phi-rational peak positions on the ladder. The module supplies definitions and one certification theorem with no complex proof steps.

claimThe wavenumber at the n-th CMB acoustic peak is given by $k_n = k_0 φ^n$, where φ is the self-similar fixed point. Adjacent peak ratios are scale-invariant and satisfy explicit algebraic relations derived from the Recognition Composition Law.

background

Recognition Science places structure formation on the phi-ladder that emerges from the eight-tick octave and the J-cost functional. The module introduces k_peak as the direct scaling k_n = k_0 φ^n and supplies helper functions k_peak_pos, k_peak_adjacent_ratio, peak_2_1_ratio and peak_3_2_ratio. Upstream it imports the fundamental RS time quantum τ₀ = 1 tick from Constants, which anchors all rung indices on the ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the phi-rational skeleton required by the downstream CMBAcousticPeakRatios theorem, which adds numerical-band predictions for the first three acoustic-peak ratios and a direct comparison to Planck 2018 data. It completes Track E1 of Plan v5 by fixing the wavenumber positions before ratio analysis begins.

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)