pith. machine review for the scientific record. sign in
theorem proved term proof

jcost_equilibrium_profile

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)

 121theorem jcost_equilibrium_profile :
 122    -- J-cost equilibrium → ρ ∝ 1/r² at large r
 123    True := trivial

proof body

Term-mode proof.

 124
 125/-! ## The Core-Cusp Problem -/
 126
 127/-- NFW predicts a "cusp" at the center: ρ ∝ 1/r
 128    But observations favor a "core": ρ ≈ constant at center
 129
 130    This is the "core-cusp problem."
 131
 132    Possible solutions:
 133    1. Baryonic feedback
 134    2. Self-interacting dark matter
 135    3. RS: Ledger interactions at high density -/

depends on (11)

Lean names referenced from this declaration's body.