rs_minkowski_eq

formal source

  63def rs_minkowski : MetricTensor := minkowski_tensor
  64
  65/-- The RS-derived MetricTensor is exactly the IM minkowski_tensor. -/
  66theorem rs_minkowski_eq : rs_minkowski = minkowski_tensor := rfl
  67
  68/-! ## §2 Diagonal Component Theorems -/
  69
  70theorem rs_eta_00 : rs_eta 0 0 = -1 := by simp [rs_eta]
  71theorem rs_eta_11 : rs_eta 1 1 = 1 := by simp [rs_eta]
  72theorem rs_eta_22 : rs_eta 2 2 = 1 := by simp [rs_eta]
  73theorem rs_eta_33 : rs_eta 3 3 = 1 := by simp [rs_eta]
  74
  75theorem rs_eta_offdiag (i j : Fin 4) (h : i ≠ j) : rs_eta i j = 0 := by
  76  simp [rs_eta, h]
  77
  78theorem rs_eta_symm (i j : Fin 4) : rs_eta i j = rs_eta j i := by
  79  unfold rs_eta
  80  by_cases h : i = j
  81  · subst h; rfl
  82  · simp [h, Ne.symm h]
  83
  84/-! ## §3 Christoffel Symbols: Real vs Scaffold
  85
  86The scaffold `Connection.christoffel_from_metric` returns Γ = 0 for all metrics.
  87The real `Curvature.christoffel` computes the Levi-Civita symbols from ∂g.
  88For Minkowski, both give zero, but for curved metrics they differ.
  89
  90This section proves that `Curvature.christoffel` is the correct one to use
  91and that for Minkowski they agree. -/
  92
  93/-- For Minkowski, the real Christoffel symbols vanish. -/
  94theorem minkowski_real_christoffel_zero (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) :
  95    christoffel minkowski_tensor x ρ μ ν = 0 :=
  96  minkowski_christoffel_zero_proper x ρ μ ν