riemann_lowered_first_bianchi
plain-language theorem explainer
The lowered Riemann tensor obeys the cyclic sum identity R_ρσμν + R_ρμνσ + R_ρνσμ = 0. Relativists using coordinate-basis curvature would cite this when the metric lowers the first index of the standard Bianchi relation. The argument contracts the mixed-tensor identity with the metric, distributes the sum, and reduces the inner expression to zero.
Claim. For any metric tensor $g$, point $x$ in four-dimensional space, and indices $ρ,σ,μ,ν$, the lowered Riemann components satisfy $R_{ρσμν} + R_{ρμνσ} + R_{ρνσμ} = 0$.
background
The module derives symmetry properties of the Riemann curvature tensor from its definition via Christoffel symbols. MetricTensor supplies a local bilinear form on four-dimensional space. The lowered Riemann tensor is the metric contraction of the mixed tensor in the first index. The upstream mixed-tensor first Bianchi identity supplies the cyclic sum on the contravariant index that is contracted here.
proof idea
Unfold the lowered definition, apply sum-additivity twice to distribute the metric factor, invoke the mixed first Bianchi identity on the inner sum, then multiply the result by zero.
why it matters
This supplies the lowered first Bianchi identity required by the algebraic derivation of pair-exchange symmetry in the downstream riemann_lowered_pair_exchange theorem. It completes the trio of properties (first-pair antisymmetry, second-pair antisymmetry, and Bianchi) used to obtain R_ρσμν = R_μνρσ. The result matches the standard coordinate-basis treatment referenced in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.