Navier–Stokes Comparator submission: options (C) and (D)

Expose the project's proof adapters under the reference theorem names. The adapters import ComparatorDefinitions, never the challenge module.

theorem NavierStokes.Comparator.navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)), InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧ ¬∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), NavierStokesExistenceAndSmoothnessRn nu u₀ f v p

(C) Breakdown of Navier–Stokes solutions on ℝ³.

theorem NavierStokes.Comparator.navier_stokes_breakdown_periodic (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)), InitialVelocityConditionPeriodic u₀ ∧ ForceConditionPeriodic f ∧ ¬∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), NavierStokesExistenceAndSmoothnessPeriodic nu u₀ f v p

(D) Breakdown of Navier–Stokes solutions on ℝ³/ℤ³.