FlatChain

formal source

  77    J(1+ε) = ε²/2 + O(ε⁴)  →  spatial metric g_ij = δ_ij  →
  78    η = diag(-1,+1,+1,+1)  →  Γ = 0  →  R^ρ_σμν = 0  →
  79    R_μν = 0  →  R = 0  →  G_μν = 0 -/
  80structure FlatChain : Prop where
  81  minkowski_christoffel : ∀ x ρ μ ν,
  82    christoffel minkowski_tensor x ρ μ ν = 0
  83  minkowski_riemann : ∀ x up low,
  84    riemann_tensor minkowski_tensor x up low = 0
  85  minkowski_ricci : ∀ x up low,
  86    ricci_tensor minkowski_tensor x up low = 0
  87  minkowski_scalar : ∀ x,
  88    ricci_scalar minkowski_tensor x = 0
  89  minkowski_einstein : ∀ x up low,
  90    einstein_tensor minkowski_tensor x up low = 0
  91
  92/-- The flat chain holds. All fields proved in `Curvature.lean`. -/
  93theorem flat_chain_holds : FlatChain where
  94  minkowski_christoffel := minkowski_christoffel_zero_proper
  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. -/
 107structure WeakFieldBridge where
 108  potential : (Fin 4 → ℝ) → ℝ
 109  density : (Fin 4 → ℝ) → ℝ
 110  poisson : ∀ x, laplacian potential x = (1/2 : ℝ) * 8 * phi ^ 5 * density x