Cosmology Void Topology From Config Dim Void Class Count

Five void classes

Cosmic voids are the large, nearly empty regions between galaxy filaments in the large-scale structure of the universe. Astronomers do not find them by one method alone. Different surveys and different questions call for different ways of drawing a void's boundary. The standard practice has settled on five canonical classes: VIDE/ZOBOV voids (named for the Void IDentification and Evaluation toolkit and its watershed algorithm), watershed voids, underdensity voids, dynamical voids, and supervoids larger than 100 megaparsecs.

The Recognition Science framework's machine-checked library of formal theorems records this classification as a finite list. Its declaration voidClass_count states that the number of these classes is exactly five. The proof is a direct computation: the library defines the five classes as an inductive type, then verifies by deciding that the type has exactly five elements. The declaration is a theorem with no unproved assumptions and no axioms beyond the ambient type theory.

What the declaration does not claim is where its real content lies. It does not say that these five classes are physically exhaustive, that every void in the universe belongs to exactly one class, or that the classification is complete for all time. It does not assert that the five classes are mutually exclusive, nor that any particular void-finding algorithm is superior. It makes no claim about the actual distribution, size, or number of voids in the observed universe. The theorem is about the framework's own definitional choice: it counts the classes as the framework has chosen to model them.

In Recognition Science, this count connects to a broader pattern. The framework derives many structural constants from a single forcing chain, and the number five here matches the dimension of the configuration space used in the framework's cosmology module. The declaration acts as a certification: it pins down the vocabulary of void classification so that later theorems can refer to a fixed, finite set of classes without ambiguity. The payoff is not a new astronomical discovery but a precise foundation for further formal work.

inductive VoidClass where
  | vide
  | watershed
  | underdensity
  | dynamical
  | supervoid
  deriving DecidableEq, Repr, BEq, Fintype

theorem voidClass_count : Fintype.card VoidClass = 5 := by decide

theorem voidClass_count : Fintype.card VoidClass = 5 := by decide

What this page does not claim

The five classes are physically exhaustive or mutually exclusive in the observed universe. Any particular void-finding algorithm is superior to the others. The declaration makes any claim about the actual number or distribution of voids in the cosmos.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/VoidTopologyFromConfigDim.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: