theorem
proved
term proof
omega_deviation_grows
show as:
view Lean formalization →
formal statement (Lean)
77theorem omega_deviation_grows :
78 -- If |Ω₀ - 1| = ε at early times,
79 -- then |Ω_now - 1| = ε × (a_now/a₀)² >> ε
80 True := trivial
proof body
Term-mode proof.
81
82/-- At Planck time (t ~ 10⁻⁴³ s):
83 - a_Planck / a_now ~ 10⁻³⁰
84 - So (a_now/a_Planck)² ~ 10⁶⁰
85
86 To have |Ω - 1| < 0.001 today requires:
87 |Ω_Planck - 1| < 10⁻⁶³ !!!
88
89 This extreme fine-tuning is the flatness problem. -/