k_peak_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not fix the absolute value of the base scale k_0.
- Does not compute power-spectrum amplitudes or growth factors.
- Does not incorporate redshift or late-time expansion effects.
- Does not address peaks beyond the first three acoustic modes.
formal statement (Lean)
42theorem k_peak_pos (k_0 : ℝ) (n : ℕ) (h : 0 < k_0) :
43 0 < k_peak k_0 n := by
proof body
Term-mode proof.
44 unfold k_peak
45 exact mul_pos h (pow_pos phi_pos n)
46
47/-- Adjacent peak ratio is exactly `φ`. -/