pith. machine review for the scientific record. sign in
def definition def or abbrev

predictions

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 209def predictions : List String := [

proof body

Definition body.

 210  "Flat rotation curves from ledger equilibrium",
 211  "Cores at centers (not cusps)",
 212  "Tully-Fisher relation M ∝ v⁴",
 213  "MOND-like at low accelerations",
 214  "DM/baryon ratio ~ φ³+1 ≈ 5"
 215]
 216
 217/-! ## Summary -/
 218
 219/-- RS explanation of galaxy rotation:
 220
 221    1. **Ledger shadows**: Dark matter is odd-phase ledger
 222    2. **Halo distribution**: J-cost equilibrium → ρ ∝ 1/r²
 223    3. **Flat curves**: M(r) ∝ r → v = constant
 224    4. **Cores**: Ledger interaction prevents cusp
 225    5. **Tully-Fisher**: Natural from J-cost -/

depends on (18)

Lean names referenced from this declaration's body.