theorem proved term proof

`keplerian_falloff`

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

formal statement (Lean)

  59theorem keplerian_falloff :
  60    -- v ∝ 1/√r for point mass
  61    True := trivial

Term-mode proof.

  62
  63/-- The observed flat rotation curve:
  64    v ≈ 200-300 km/s for most spirals
  65    Roughly constant from ~5 kpc to ~30+ kpc! -/

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use