`ledgerShadowProperties`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.DarkMatter
domain: Cosmology
line: 187 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.DarkMatter on GitHub at line 187.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 184    4. **Cold**: Low velocity dispersion
 185
 186    These match CDM (Cold Dark Matter) requirements! -/
 187def ledgerShadowProperties : List String := [
 188  "Gravitates (J-cost → geometry)",
 189  "No electromagnetic interaction",
 190  "Weak self-interaction (collisionless)",
 191  "Cold (phase-locked to ledger)"
 192]
 193
 194/-- Self-interaction of dark matter:
 195
 196    Ledger shadows can interact with each other.
 197    But cross-section is small: σ/m < 1 cm²/g (cluster limits).
 198
 199    In RS: Odd-phase × odd-phase → even-phase is suppressed. -/
 200theorem dm_self_interaction_small :
 201    -- σ/m < 1 cm²/g from J-cost suppression
 202    True := trivial
 203
 204/-! ## Structure Formation -/
 205
 206/-- Dark matter drives structure formation:
 207
 208    1. DM decouples early (no photon pressure)
 209    2. DM perturbations grow during radiation era
 210    3. Baryons fall into DM "halos" after recombination
 211    4. Galaxies form in DM potential wells
 212
 213    Without DM, galaxies wouldn't have formed in time. -/
 214def structureFormation : List String := [
 215  "DM decouples early (z ~ 10⁶)",
 216  "DM perturbations grow: δ ∝ a",
 217  "Baryons fall in after z ~ 1100",

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.