pith. sign in
module module moderate

IndisputableMonolith.Cosmology.DarkMatter

show as:
view Lean formalization →

This module defines the dark matter density parameter Ω_dm and related quantities in the Recognition Science cosmology. Cosmologists working in the RS framework would cite it to express dark sector contributions via the phi-ladder and J-cost. The module consists of a collection of definitions and sector distinctions with no embedded proofs.

claimThe dark matter density parameter $Ω_{dm}$ together with $Ω_b$, the ratio $Ω_{dm}/Ω_b$, and the partition into darkSector and visibleSector, all expressed in RS-native units derived from the J-cost ledger.

background

The module imports the fundamental RS time quantum τ₀ = 1 tick from Constants, the J-cost structure from Cost, and the self-similarity argument from PhiForcing. PhiForcing establishes that φ is forced by self-similarity in a discrete ledger with J-cost, providing the fixed point used for all scaling relations. Dark matter is treated as the ledger content outside the visible phi-ladder rungs, consistent with the eight-tick octave and D = 3 spatial dimensions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions supply the dark matter sector for larger RS cosmology calculations that connect to the forcing chain T5–T8 and the Recognition Composition Law. The module distinguishes dark and visible sectors to support density parameter computations that feed downstream cosmological models.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (22)