Omega_0_pos
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.
claimLet Ω₀ := 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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of Ω₀.
- Does not derive the functional form of Ω₀ from the recognition composition law.
- Does not address observational constraints on the modulation amplitude.
Lean usage
have h : 0 < Omega_0 := Omega_0_posformal statement (Lean)
91theorem Omega_0_pos : 0 < Omega_0 := by
proof body
Term-mode proof.
92 unfold Omega_0
93 apply div_pos (mul_pos (by norm_num) Real.pi_pos)
94 apply Real.log_pos
95 rw [one_lt_div phi_pos]
96 exact lt_of_lt_of_le (by linarith [phi_lt_two]) (le_of_lt Real.pi_gt_three)
97
98/-! ## UV Knee -/
99
100/-- The UV knee (comoving): k_rec,com ≈ 1.4 × 10⁶ Mpc⁻¹.
101 Above this scale, the recognition lattice structure becomes visible
102 and the primordial spectrum softens. -/