pith. machine review for the scientific record. sign in
theorem proved term proof

X_opt_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  80theorem X_opt_pos : 0 < X_opt := div_pos phi_pos Real.pi_pos

proof body

Term-mode proof.

  81
  82/-- The log-periodic modulation frequency:
  83    Ω₀ = 2π / ln(1/X_opt) = 2π / ln(π/φ).
  84    Numerically: π/φ ≈ 1.942, ln(1.942) ≈ 0.664, so Ω₀ ≈ 9.47.
  85
  86    This produces oscillations in the primordial power spectrum
  87    with period Δln(k) = 2π/Ω₀ ≈ 0.664. -/

depends on (3)

Lean names referenced from this declaration's body.