pith. sign in
module module moderate

IndisputableMonolith.Cosmology.VoidTopologyFromConfigDim

show as:
view Lean formalization →

The Cosmology.VoidTopologyFromConfigDim module supplies definitions for VoidClass, voidClass_count, VoidTopologyCert and voidTopologyCert that derive void topology from configuration dimension in Recognition Science cosmology. Cosmologists working in the RS framework would cite these objects when connecting configuration space to observed large-scale voids. This is a definition module containing no proofs.

claim$VoidClass$, $voidClass_count$, $VoidTopologyCert$, $voidTopologyCert$ relating configuration dimension to void topology in RS cosmology.

background

This module sits in the Cosmology domain and imports only Mathlib plus IndisputableMonolith.Constants, whose sole documented object is the RS time quantum τ₀ = 1 tick. It introduces four sibling definitions that classify voids and certify their topology once configuration dimension is fixed. The surrounding Recognition Science setting uses the J-functional equation, the phi-ladder for mass scales, and the eight-tick octave to constrain spatial structure.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply the basic objects needed for any later cosmology theorems that treat void topology as a derived consequence of configuration dimension. No downstream uses are recorded yet, so the module currently stands as scaffolding for larger RS cosmology derivations that would invoke T8 (D = 3) or the phi-ladder.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)