StructureFormationFromBITCert
plain-language theorem explainer
StructureFormationFromBITCert encodes the four φ-ladder properties of CMB acoustic peak wavenumbers k_n = k_0 φ^n derived from the BIT kernel. Cosmologists modeling structure formation cite it to obtain parameter-free ratio predictions for the matter power spectrum. The declaration is a structure definition assembled directly from four sibling lemmas on positivity, adjacent ratios, the φ² relation for peaks 3 and 1, and scale invariance.
Claim. The structure asserts that for every positive base wavenumber $k_0$, the sequence $k_n = k_0 φ^n$ satisfies $k_n > 0$ for all $n$, the adjacent ratio $k_{n+1}/k_n = φ$, the specific ratio $k_3/k_1 = φ^2$, and that all such ratios remain unchanged when the positive base $k_0$ is replaced by any other positive $k_0'$.
background
The module derives the matter power spectrum from the BIT kernel, so that characteristic wavenumbers form a φ-ladder: k_peak(k_0, n) is defined as k_0 · φ^n. This definition supplies the n-th acoustic peak location once a positive base scale k_0 is chosen. Upstream lemmas establish positivity of every k_peak when k_0 > 0 and the algebraic consequences of the self-similar fixed point φ.
proof idea
The declaration is a structure definition. Its four fields are supplied by the sibling lemmas k_peak_pos, k_peak_adjacent_ratio, peak_3_1_ratio, and peak_ratios_scale_invariant. The downstream constructor structureFormationFromBITCert simply packages these four lemmas into a single inhabited certificate.
why it matters
The certificate realizes Track F4 by embedding the φ-ladder into cosmological structure formation, confirming that the first three CMB acoustic peaks obey the ratios φ and φ². It supplies the parent theorem structureFormationFromBITCert, which closes the parameter-free prediction for peak ratios. The module states the explicit falsifier: any observed ratio more than 5 % off the predicted φ or φ² values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.