flat_chain_holds

formal source

  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
 111
 112/-! ## §4 Coupling Constant Chain -/
 113
 114/-- The Einstein coupling κ = 8πG/c⁴ = 8φ⁵ in RS-native units.
 115    This is derived in `Constants.lean` and `ZeroParameterGravity.lean`. -/
 116theorem coupling_from_phi : (8 : ℝ) * phi ^ (5 : ℝ) > 0 := by
 117  apply mul_pos (by norm_num : (8 : ℝ) > 0)
 118  exact Real.rpow_pos_of_pos phi_pos 5
 119
 120/-! ## §5 Regge Convergence Hypothesis -/
 121
 122/-- Non-degeneracy of the metric matrix at a point.
 123    This mirrors the variational layer's invertibility hypothesis without