theorem proved term proof

`isothermal_halo`

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

formal statement (Lean)

  87theorem isothermal_halo :
  88    -- ρ ∝ 1/r² gives flat rotation curve
  89    True := trivial

proof body

Term-mode proof.

  90
  91/-- The NFW (Navarro-Frenk-White) profile:
  92    ρ(r) = ρ_s / [(r/r_s)(1 + r/r_s)²]
  93
  94    - Inner: ρ ∝ 1/r (cuspy)
  95    - Outer: ρ ∝ 1/r³ (steeper than isothermal)
  96
  97    From N-body simulations of CDM. -/

depends on (5)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use