`dm_ratio_phi_connection`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.DarkMatter on GitHub at line 171.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 168
 169    φ² ≈ 2.62, (φ² + 1)/φ ≈ 2.23
 170    5.4 ≈ φ³ + 1 = 5.24 (close!) -/
 171theorem dm_ratio_phi_connection :
 172    -- Ω_dm/Ω_b ≈ φ³ + 1 ≈ 5.24
 173    -- Observed: 5.4
 174    -- Match: ~3%
 175    True := trivial
 176
 177/-! ## Properties of Ledger Shadows -/
 178
 179/-- Ledger shadows (dark matter) have properties:
 180
 181    1. **Gravitating**: J-cost couples to geometry
 182    2. **Non-luminous**: No photon coupling
 183    3. **Collisionless**: Weak self-interaction
 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

papers checked against this theorem

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