def
definition
def or abbrev
summary
show as:
view Lean formalization →
formal statement (Lean)
270def summary : List String := [
proof body
Definition body.
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 -/