voidClass_count
The theorem establishes that the inductive type enumerating five standard cosmic void categories has finite cardinality exactly five. Large-scale structure cosmologists would cite this count when certifying completeness of void topology models at configuration dimension five. The proof is a direct decision procedure that exhausts the five constructors of the finite inductive type.
claimThe finite cardinality of the type of void classes is five: $ |VoidClass| = 5 $.
background
VoidClass is the inductive type with constructors vide, watershed, underdensity, dynamical, and supervoid. These label the five canonical void finders in large-scale structure: VIDE/ZOBOV voids, watershed voids, underdensity voids, dynamical voids, and supervoids exceeding 100 Mpc. The module derives cosmic void topology from this fixed enumeration at configuration dimension D = 5, with zero axioms or sorrys.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. Decide succeeds because the inductive type derives a Fintype instance, allowing exhaustive enumeration of its five constructors to compute the cardinality.
why it matters in Recognition Science
This supplies the five_classes field inside the VoidTopologyCert definition, which certifies the void topology structure for the module. It directly realizes the five-class count stated in the module documentation for configDim D = 5. In the Recognition Science setting it discretizes topological features at the scale where the eight-tick octave forces D = 3, though explicit ties to the J-function or Recognition Composition Law remain outside this declaration.
scope and limits
- Does not derive the five-class taxonomy from the forcing chain or J-uniqueness.
- Does not compute void number densities or size distributions.
- Does not connect to the phi-ladder mass formula or Berry threshold.
- Does not address observational selection effects in void catalogs.
Lean usage
have h : Fintype.card VoidClass = 5 := voidClass_countformal statement (Lean)
24theorem voidClass_count : Fintype.card VoidClass = 5 := by decide
proof body
25