93theorem flat_chain_holds : FlatChain where 94 minkowski_christoffel := minkowski_christoffel_zero_proper
proof body
Term-mode proof.
95 minkowski_riemann := minkowski_riemann_zero 96 minkowski_ricci := minkowski_ricci_zero 97 minkowski_scalar := minkowski_ricci_scalar_zero 98 minkowski_einstein := minkowski_einstein_zero 99 100/-! ## §3 Weak-Field Limit -/ 101 102/-- In the weak-field limit g_μν = η_μν + h_μν with |h| << 1, 103 the linearized Einstein equations reduce to the Poisson equation 104 ∇²Φ = (κ/2) ρ, where Φ = -h_{00}/2 and ρ is mass density. 105 106 This is the bridge from curvature to Newtonian gravity. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.