def
definition
def or abbrev
summary
show as:
view Lean formalization →
formal statement (Lean)
226def summary : List String := [
proof body
Definition body.
227 "Dark matter = ledger shadows",
228 "Halo from J-cost equilibrium",
229 "Flat curves from ρ ∝ 1/r²",
230 "Cores from ledger interactions",
231 "Tully-Fisher from J-cost"
232]
233
234/-! ## Falsification Criteria -/
235
236/-- The derivation would be falsified if:
237 1. Rotation curves not flat (already confirmed)
238 2. No dark matter (MOND works everywhere)
239 3. Ledger distribution doesn't match observations -/