rs_eta_33

formal source

  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 ρ μ ν
  97
  98/-- The old zero-valued scaffold agrees with the real Christoffel on Minkowski. -/
  99theorem scaffold_agrees_on_minkowski (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) :
 100    (0 : ℝ) = christoffel minkowski_tensor x ρ μ ν := by
 101  simp [minkowski_real_christoffel_zero]
 102
 103/-! ## §4 Geodesic Structures Using Real Christoffel Symbols