riemann_first_bianchi
plain-language theorem explainer
The first Bianchi identity asserts that the cyclic sum of the Riemann curvature tensor vanishes, R^ρ_σμν + R^ρ_μνσ + R^ρ_νσμ = 0, for any metric tensor in four dimensions. General relativists and differential geometers cite this identity when deriving properties of the curvature tensor or the contracted Bianchi identities. The proof expands the definition of the Riemann tensor in terms of Christoffel symbols, applies symmetry properties of the Christoffel symbols, and closes with algebraic cancellation via the ring tactic.
Claim. The cyclic sum of the Riemann curvature tensor vanishes: $R^ρ_{σμν} + R^ρ_{μνσ} + R^ρ_{νσμ} = 0$, where the Riemann tensor is constructed from the metric tensor $g$ at spacetime point $x ∈ ℝ^4$.
background
The module establishes algebraic properties of the Riemann curvature tensor from its definition in terms of Christoffel symbols of a metric. The MetricTensor structure supplies a local non-sealed bilinear form on four-dimensional space. The riemann_tensor is built from partial derivatives of Christoffel symbols together with their quadratic products, following the standard construction in general relativity.
proof idea
The proof unfolds the riemann_tensor definition, simplifies the index selector functions with Fin.val lemmas, applies partialDeriv_christoffel_sym three times to symmetrize the first derivatives of the Christoffel symbols, invokes christoffel_symmetric on the quadratic terms to align permutations, and closes with the ring tactic to obtain cancellation.
why it matters
This theorem feeds the lowered first Bianchi identity riemann_lowered_first_bianchi and the trace relation ricci_minus_transpose_eq_trace that establishes Ricci tensor symmetry. It supplies the first Bianchi identity referenced to Wald Eq. (3.2.14) and MTW Chapter 13, serving as a prerequisite for the pair-exchange symmetry derived later in the module. In the Recognition Science setting it anchors the geometric layer of the relativity module consistent with the emergence of spatial structure from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.