pith. sign in
module module moderate

IndisputableMonolith.Cosmology.DarkMatter

show as:
view Lean formalization →

The Cosmology.DarkMatter module defines the dark matter density parameter and related cosmological quantities in Recognition Science. Researchers deriving RS-native Omega_DM values from the phi-ladder would cite these definitions. The module consists of definitions that apply the J-cost and self-similar forcing structures imported from upstream modules.

claimThe dark matter density parameter $Omega_{DM}$, baryon density $Omega_b$, their ratio, and sector distinctions (visibleSector, darkSector) in RS-native units.

background

The module sits in the cosmology domain and imports the RS time quantum tau_0 = 1 tick, the J-cost structure, and the PhiForcing module. The latter proves that phi is forced by self-similarity in a discrete ledger with J-cost. It distinguishes dark and visible sectors while applying the Recognition Composition Law to density parameters.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the dark matter density parameter that supports cosmological applications of the forcing chain. It connects to T5 J-uniqueness and T6 phi fixed point via the PhiForcing import. No downstream theorems are listed.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (22)