mondStatus

formal source

 255    But: Fails for clusters, CMB, structure formation.
 256
 257    RS: Dark matter is real, not modified gravity. -/
 258def mondStatus : String :=
 259  "Works for rotation curves, fails for clusters and CMB"
 260
 261/-! ## Summary -/
 262
 263/-- RS explanation of dark matter:
 264
 265    1. **8-tick phases**: 4 visible + 4 dark
 266    2. **Ledger shadows**: Odd-phase matter
 267    3. **Gravitates but dark**: No photon coupling
 268    4. **Ratio ~ φ³+1**: Explains 5:1 ratio
 269    5. **Null detection**: Phase mismatch suppression -/
 270def summary : List String := [
 271  "8-tick gives visible and dark sectors",
 272  "Dark matter = odd-phase ledger",
 273  "Gravitates (J-cost) but doesn't shine",
 274  "Ratio Ω_dm/Ω_b ≈ φ³+1 ≈ 5.2",
 275  "Detection suppressed by phase mismatch"
 276]
 277
 278/-! ## Falsification Criteria -/
 279
 280/-- The derivation would be falsified if:
 281    1. Dark matter doesn't exist (MOND works fully)
 282    2. DM ratio very different from φ³+1
 283    3. DM couples strongly to photons -/
 284structure DarkMatterFalsifier where
 285  dm_not_real : Prop
 286  ratio_wrong : Prop
 287  dm_couples_photon : Prop
 288  falsified : dm_not_real ∨ dm_couples_photon → False