VoidTopologyCert
plain-language theorem explainer
VoidTopologyCert is a structure that certifies the finite type VoidClass has cardinality exactly five. Cosmologists modeling void topology would cite it to fix configDim at D=5 for the five canonical void classes. The declaration is a bare structure definition that directly encodes the Fintype.card assertion with no further computation.
Claim. A certificate consisting of the field asserting that the cardinality of the inductive type VoidClass equals 5, where VoidClass enumerates the five constructors vide, watershed, underdensity, dynamical, and supervoid.
background
In this module VoidClass is the inductive type whose five constructors label the canonical void finders: vide, watershed, underdensity, dynamical, and supervoid. The module document states that these five classes correspond to configDim D=5 in the Recognition Science cosmology setting, with zero sorries or axioms present. The upstream result is simply the inductive definition of VoidClass itself.
proof idea
The declaration is a structure definition that directly packages the cardinality condition. No lemmas or tactics are invoked; it is a one-line wrapper around the Fintype.card equality for the VoidClass inductive type.
why it matters
This definition supplies the type used by the downstream voidTopologyCert, which constructs an explicit instance via voidClass_count. It anchors the five-class enumeration to configDim D=5 in the cosmology depth section, consistent with the framework's discrete dimensional assignments. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.