VoidClass
plain-language theorem explainer
VoidClass enumerates the five canonical void categories employed in large-scale structure surveys. Cosmologists mapping VIDE, watershed, underdensity, dynamical and supervoid populations would cite this enumeration when fixing configDim to 5. The declaration is a direct inductive construction that lists the five constructors and derives the Fintype instance used by the cardinality theorem.
Claim. Let $V$ be the inductive type whose five constructors are vide, watershed, underdensity, dynamical and supervoid. The type carries decidable equality, a representation, boolean equality and a finite-type structure.
background
The module fixes configDim at 5 to match the number of standard void classes used by cosmological void finders. These classes are VIDE/ZOBOV voids, watershed voids, underdensity voids, dynamical voids and supervoids exceeding 100 Mpc. The inductive definition supplies the discrete label set whose exact cardinality is asserted by the companion theorem voidClass_count.
proof idea
Direct inductive definition that introduces the five named constructors and derives the four type-class instances in a single declaration line.
why it matters
VoidClass provides the finite label set required by VoidTopologyCert and by the theorem that its cardinality equals 5. This choice of five classes implements the configDim parameter that sets the dimensionality of the void classification space in the Recognition Science cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.