theorem
proved
tactic proof
riemann_first_bianchi
show as:
view Lean formalization →
formal statement (Lean)
101theorem riemann_first_bianchi (g : MetricTensor) (x : Fin 4 → ℝ) (ρ σ μ ν : Fin 4) :
102 riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then σ else if i.val = 1 then μ else ν) +
103 riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then μ else if i.val = 1 then ν else σ) +
104 riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then ν else if i.val = 1 then σ else μ) = 0 := by
proof body
Tactic-mode proof.
105 -- The First Bianchi Identity: R^ρ_σμν + R^ρ_μνσ + R^ρ_νσμ = 0
106 -- Expand the Riemann tensor definition
107 unfold riemann_tensor
108 simp only [Fin.val_zero, Fin.val_one, Fin.val_two,
109 show (0 : ℕ) ≠ 1 from by decide,
110 show (1 : ℕ) ≠ 0 from by decide, show (2 : ℕ) ≠ 0 from by decide,
111 show (2 : ℕ) ≠ 1 from by decide, if_true, if_false]
112 -- Use Christoffel symmetry for partial derivatives
113 rw [partialDeriv_christoffel_sym g x ρ ν σ μ] -- ∂_μ Γ^ρ_νσ → ∂_μ Γ^ρ_σν
114 rw [partialDeriv_christoffel_sym g x ρ μ σ ν] -- ∂_ν Γ^ρ_μσ → ∂_ν Γ^ρ_σμ
115 rw [partialDeriv_christoffel_sym g x ρ ν μ σ] -- ∂_σ Γ^ρ_νμ → ∂_σ Γ^ρ_μν
116 -- Use Christoffel symmetry in the Γ·Γ products
117 simp_rw [christoffel_symmetric g x _ ν σ, christoffel_symmetric g x _ μ σ,
118 christoffel_symmetric g x _ σ μ, christoffel_symmetric g x _ ν μ,
119 christoffel_symmetric g x _ μ ν, christoffel_symmetric g x _ σ ν]
120 -- Now ring should close the goal since all terms cancel
121 ring
122
123/-- **COROLLARY**: First Bianchi for the fully lowered tensor.
124 R_ρσμν + R_ρμνσ + R_ρνσμ = 0
125
126 This follows directly from the First Bianchi identity for the mixed tensor
127 by lowering the first index with the metric:
128 Σ_α g_{ρα} (R^α_σμν + R^α_μνσ + R^α_νσμ) = Σ_α g_{ρα} · 0 = 0 -/