algebraic_bianchi
plain-language theorem explainer
The algebraic Bianchi identity asserts that the cyclic sum of Riemann tensor components over the last three indices vanishes for any torsion-free connection. Differential geometers and general relativists cite this when deriving curvature properties from Christoffel symbols in local coordinates. The proof obtains three instances of antisymmetry in the final pair of indices, expands the tensor definition, cancels the quadratic terms by repeated application of the symmetry hypotheses together with index summation, and finishes with linear-arithm.
Claim. Let $R^ρ{}_{σμν}$ be the Riemann tensor built from Christoffel symbols $Γ^ρ_{μν}$ and their first derivatives. Assume the connection is torsion-free, so $Γ^ρ_{μν}=Γ^ρ_{νμ}$ and the derivatives satisfy the corresponding symmetry. Then $R^ρ{}_{σμν}+R^ρ{}_{μνσ}+R^ρ{}_{νσμ}=0$.
background
The module Gravity.RiemannTensor constructs the Riemann tensor in four-dimensional coordinates where Idx stands for Fin 4. Its definition reads $R^ρ{}{σμν}=∂μΓ^ρ{νσ}-∂νΓ^ρ{μσ}+∑λ(Γ^ρ{μλ}Γ^λ{νσ}-Γ^ρ_{νλ}Γ^λ_{μσ})$. The immediately preceding result establishes antisymmetry in the last two indices: $R^ρ{}{σμν}=-R^ρ{}{σνμ}$. The local setting is a torsion-free affine connection on spacetime; no metric is introduced at this stage.
proof idea
Three applications of the antisymmetry theorem supply the cyclic permutations. After simp on the tensor definition, a per-index cancellation identity is proved by rewriting each quadratic pair with the symmetry hypotheses and invoking ring. These identities are summed over the index set; the derivative symmetries are substituted to align all terms, after which linarith concludes the sum is zero.
why it matters
The declaration supplies the algebraic Bianchi identity required for any subsequent curvature analysis in the gravity module. It sits directly after the tensor definition and antisymmetry lemma, completing the minimal set of algebraic properties needed before metric-compatible or differential identities can be stated. In the Recognition Science chain this coordinate identity supports the passage from the Recognition Composition Law to gravitational dynamics, though the present proof remains purely algebraic and independent of the eight-tick octave or the three-dimensional spatial reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.