79structure EnergyDistribution where 80 density : Position → ℝ 81 density_nonneg : ∀ h, 0 ≤ density h 82 83/-- The Newtonian potential sourced by an energy distribution. 84 In weak-field RS: ∇²Φ = 4πG·ρ, where ρ = J-cost density = energy density. 85 We model the 1D version: Φ(h) = -G ∫ ρ(h') |h - h'|⁻¹ dh' (schematic). 86 For the formal proof, we axiomatize the Poisson relation. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.