IndisputableMonolith.Cosmology.VoidTopologyFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Cosmic Void Topology from configDim — Cosmology Depth
   6
   7Five canonical void-finder/void-type classes (= configDim D = 5):
   8  VIDE/ZOBOV voids, watershed voids, underdensity voids,
   9  dynamical voids, supervoids (> 100 Mpc).
  10
  11Lean status: 0 sorry, 0 axiom.
  12-/
  13
  14namespace IndisputableMonolith.Cosmology.VoidTopologyFromConfigDim
  15
  16inductive VoidClass where
  17  | vide
  18  | watershed
  19  | underdensity
  20  | dynamical
  21  | supervoid
  22  deriving DecidableEq, Repr, BEq, Fintype
  23
  24theorem voidClass_count : Fintype.card VoidClass = 5 := by decide
  25
  26structure VoidTopologyCert where
  27  five_classes : Fintype.card VoidClass = 5
  28
  29def voidTopologyCert : VoidTopologyCert where
  30  five_classes := voidClass_count
  31
  32end IndisputableMonolith.Cosmology.VoidTopologyFromConfigDim
  33