VoidClass
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not encode density thresholds or selection criteria that distinguish the five classes.
- Does not derive topological invariants or connectivity relations among voids.
- Does not connect the classes to the Recognition forcing chain or phi-ladder.
- Does not treat survey selection functions or completeness corrections.
Lean usage
import IndisputableMonolith.Cosmology.VoidTopologyFromConfigDim theorem card_check : Fintype.card VoidClass = 5 := by decideformal statement (Lean)
16inductive VoidClass where
17 | vide
18 | watershed
19 | underdensity
20 | dynamical
21 | supervoid
22 deriving DecidableEq, Repr, BEq, Fintype
23