peak_3_1_ratio
plain-language theorem explainer
The ratio of the third to first CMB acoustic peak wavenumber equals phi squared for any positive base scale. Structure-formation modelers in Recognition Science cite this to establish the phi-ladder in the matter power spectrum. The proof unfolds the k_peak definition and cancels algebraically after confirming nonzero factors.
Claim. For any positive real $k_0$, the ratio of the third acoustic-peak wavenumber to the first satisfies $k_3 / k_1 = phi^2$, where the wavenumber at tier $n$ is defined by $k_n = k_0 phi^n$.
background
The module derives the matter power spectrum from the BIT kernel, inheriting a phi-ladder of wavenumbers $k_n = k_0 phi^n$. The definition of $k_peak$ supplies the explicit scaling $k_n = k_0 phi^n$ with all peaks positive for positive $k_0$. Upstream results include the scale function from LargeScaleStructureFromRS that supplies the same phi-power and the independent spatial semantics from LNALSemantics that keep voxels non-interacting at this stage.
proof idea
Unfold the definition of k_peak to obtain the explicit ratio $(k_0 phi^3) / (k_0 phi^1)$. Establish phi nonzero from phi_pos and k_0 nonzero from the hypothesis. Apply field_simp to cancel the common factors and obtain phi squared.
why it matters
This result populates the master certificate structureFormationFromBITCert and is invoked verbatim by ratio_3_1 in CMBAcousticPeakRatios. It supplies the phi-rational structure for the first three peaks required by the module's theorem statement, closing the parameter-free ratio sector of the BIT-derived spectrum and aligning with the self-similar fixed point of T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.