peak_ratios_scale_invariant
plain-language theorem explainer
Ratios of CMB acoustic peak wavenumbers separated by m steps equal phi to the power m and stay unchanged when the base scale k_0 is replaced by any other positive k_0'. Modelers of structure formation from the BIT kernel cite the result to obtain parameter-free ratios in the power spectrum. The proof unfolds the explicit form of k_peak, cancels the base-scale factors via exponent addition and field simplification, and verifies both sides reduce to the same phi^m.
Claim. For positive reals $k_0$ and $k_0'$, and natural numbers $n,m$, the ratio of peak wavenumbers satisfies $k_0 phi^{n+m}/(k_0 phi^n) = k_0' phi^{n+m}/(k_0' phi^n)$, where the peak wavenumber at step $n$ is defined by $k_n = k_0 phi^n$.
background
The module develops the matter power spectrum from the BIT kernel and shows that it inherits a phi-ladder of characteristic wavenumbers. The auxiliary definition k_peak(k_0, n) := k_0 * phi^n encodes the n-th acoustic peak; positivity of all peaks follows when k_0 > 0. The local setting is Track F4, which links the eight-tick periodicity to three spatial dimensions and supplies the self-similar fixed point phi used throughout the ladder.
proof idea
The tactic proof unfolds k_peak on both sides of the target equality. It introduces three non-zero facts (phi, k_0, k_0') and the corresponding power non-zero facts, then reduces each ratio separately: the left-hand side becomes phi^m by pow_add and field_simp, and the right-hand side follows identically. The two simplified expressions are substituted back to close the goal.
why it matters
The result is collected inside the master certificate structureFormationFromBITCert, which packages scale invariance together with positivity and the explicit ratios k_2/k_1 = phi, k_3/k_2 = phi. It realizes the module claim that peak ratios are parameter-free constants of phi. In the Recognition framework the theorem confirms that the phi-ladder structure forced by the BIT kernel propagates unchanged into cosmological structure formation, consistent with the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.