Omega_0_pos
plain-language theorem explainer
Omega_0 is shown positive because pi/phi exceeds 1. Cosmologists modeling log-periodic modulations in the primordial spectrum cite this to confirm the frequency is well-defined. The proof is a term-mode verification that unfolds the definition and chains positivity of pi, the logarithm, and the bound phi < 2.
Claim. Let $Omega_0 := 2 pi / ln(pi / phi)$. Then $0 < Omega_0$.
background
The module formalizes RS inflationary predictions where the alpha-attractor equals phi squared and the log-periodic modulation frequency is defined as Omega_0 = 2 pi / ln(pi / phi), producing oscillations in the primordial power spectrum with period 2 pi / Omega_0. The definition of Omega_0 appears in the same module and rests on the optimal recognition ratio X_opt = phi / pi. Upstream results supply the lemma phi < 2 from Constants, PhiForcing, and related modules, which establishes pi/phi > 1 and thereby the positivity of the logarithm argument.
proof idea
The proof unfolds Omega_0 then applies div_pos to the product of a positive constant and pi with the positive logarithm of pi/phi. It rewrites the logarithm argument and invokes lt_of_lt_of_le using phi_lt_two together with pi > 3.
why it matters
This result supplies the modulation_positive field inside inflation_cert, which certifies the full set of inflationary predictions. It supports the log-periodic modulation Omega_0 approx 9.47 derived from X_opt = phi / pi. The framework landmark is the self-similar fixed point phi from the forcing chain (T5-T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.