strong_cosmic_censorship
Provedpdes
Penrose's strong cosmic censorship: Generic singularities in general relativity are always hidden behind event horizons (not visible to outside observers). The Cauchy horizon of maximal Cauchy developments is not extendible as a solution. Open; recent counterexamples for charged black holes (Dafermos–Luk 2017).
Preamble
import Mathlib
Formal statement
import Mathlib
theorem strong_cosmic_censorship :
∀ (u : ℝ → ℝ × ℝ × ℝ → ℝ) (v : ℝ → ℝ × ℝ × ℝ → ℝ),
(∀ t : ℝ, ContDiff ℝ ⊤ (u t)) →
(∀ t : ℝ, ContDiff ℝ ⊤ (v t)) →
∃ (T : ℝ), 0 < T ∧
∀ t : ℝ, t < T →
(∃ sol : ℝ → ℝ × ℝ × ℝ → ℝ, ContDiff ℝ ⊤ (sol t)) := by
sorrySource