Omega_0_pos
plain-language theorem explainer
The positivity of the log-periodic modulation frequency Ω₀ = 2π / ln(π/φ) follows from π/φ > 1. Cosmologists citing RS-derived inflation models reference this to confirm the oscillatory signature in the primordial spectrum is well-defined. The proof is a short term-mode reduction that unfolds the definition, applies div_pos and log_pos, then invokes the bound φ < 2 together with π > 3.
Claim. Let Ω₀ := 2π / ln(π/φ). Then 0 < Ω₀.
background
In the Inflation module the log-periodic modulation frequency is introduced as Ω₀ = 2π / ln(π/φ), where φ denotes the golden ratio. This quantity sets the frequency of oscillations in the primordial power spectrum with period Δln(k) = 2π/Ω₀. The module formalizes RS inflationary predictions: α = φ², n_s ≈ 1 - 2/N, r ≈ 12φ²/N², and the modulation term itself.
proof idea
The proof unfolds Omega_0, applies div_pos to a positive numerator built from 2, π and the positive denominator, then uses log_pos after rewriting the argument via one_lt_div. It closes the inequality π/φ > 1 by linarith on phi_lt_two (φ < 2) against π > 3.
why it matters
Omega_0_pos supplies the modulation_positive field inside inflation_cert, which certifies the complete set of RS inflationary predictions. It thereby anchors the log-periodic term Ω₀ ≈ 9.47 required by the Universe-Origin Paper. The result sits inside the phi-forcing chain and ensures the eight-tick octave structure yields a positive, observable modulation frequency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.