voidTopologyCert
plain-language theorem explainer
voidTopologyCert constructs an instance of the VoidTopologyCert structure by populating its five_classes field with the established cardinality of VoidClass. Cosmologists modeling void topology in Recognition Science would cite it to confirm that exactly five classes satisfy the configDim equals five requirement. The construction is a direct one-line wrapper around the decided theorem that computes the finite cardinality.
Claim. The certificate VoidTopologyCert is defined by setting its field five_classes to the value satisfying $Fintype.card(VoidClass) = 5$.
background
VoidClass is the finite type whose elements are the five canonical void classes: VIDE/ZOBOV voids, watershed voids, underdensity voids, dynamical voids, and supervoids exceeding 100 Mpc. The module VoidTopologyFromConfigDim treats configDim equal to five as the direct source of this enumeration in the Recognition Science cosmology setting. The upstream theorem voidClass_count establishes $Fintype.card(VoidClass) = 5$ by a decision procedure and supplies the concrete value inserted into the structure.
proof idea
The definition is a one-line wrapper that applies the theorem voidClass_count to fill the five_classes field of the VoidTopologyCert structure.
why it matters
This definition supplies the concrete certificate required by the cosmology module to link void topology to configDim equal to five. It closes the local construction in a module that reports zero axioms and zero sorrys, feeding any larger cosmology theorems that depend on a verified class count. The placement aligns with the framework's use of configuration dimension to fix discrete structures such as the eight-tick octave and spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.