k_peak_pos
plain-language theorem explainer
The theorem shows that every wavenumber k_n on the BIT-derived φ-ladder is strictly positive whenever the base scale k_0 is positive. Cosmologists constructing the matter power spectrum from the Recognition kernel would cite it to place all acoustic peaks in the physical domain. The proof is a one-line term wrapper that unfolds the definition of k_peak and applies the positivity of multiplication together with the positivity of powers of phi.
Claim. Let $k_0 > 0$ be real and $n$ a natural number. Then the wavenumber at the $n$-th peak satisfies $k_n > 0$, where $k_n := k_0 φ^n$.
background
The module derives the matter power spectrum P(k) from the BIT kernel, so that characteristic wavenumbers form a φ-ladder k_n = k_0 · φ^n. The upstream definition k_peak (line 39) supplies exactly this expression, while the module doc states that adjacent-peak ratios equal φ independently of the base scale k_0. The local theoretical setting is the φ-rational structure for the first three CMB acoustic peaks, with ratios φ and φ², as part of the T5–T8 forcing chain that fixes D = 3 and the eight-tick octave.
proof idea
The proof is a one-line term-mode wrapper. It unfolds k_peak to expose the product k_0 * phi^n, then applies mul_pos to the hypothesis 0 < k_0 together with pow_pos applied to the already-established positivity of phi.
why it matters
This result supplies the k_pos field of the master certificate structureFormationFromBITCert, which certifies the full φ-ladder structure for structure formation. It closes the positivity requirement inside the Recognition Composition Law and the T5 J-uniqueness step, ensuring the wavenumber ladder is well-defined before ratio theorems are applied. The module targets the first three CMB peaks with exact φ ratios; any observed deviation beyond 5 % would falsify the claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.