riemann_trace_vanishes
plain-language theorem explainer
The Riemann tensor trace vanishes under the hypothesis that encodes the contracted first Bianchi identity for a given metric tensor. General relativists cite this when establishing Ricci tensor symmetry from the algebraic properties of curvature. The proof is a one-line wrapper that directly applies the supplied hypothesis.
Claim. Under the hypothesis $H(g,x,μ,ν)$ that the first Bianchi identity contracts to relate the Riemann trace to the antisymmetric part of the Ricci tensor for metric $g$ at coordinate point $x$, the trace vanishes: $∑_ρ R^ρ_{ρμν}(g,x)=0$.
background
The module derives algebraic symmetries of the Riemann curvature tensor from its definition via Christoffel symbols of the metric. The MetricTensor structure supplies a symmetric bilinear form on Fin 4 indices at each spacetime point. Upstream results include the first Bianchi identity $R_{ρσμν} + R_{ρμνσ} + R_{ρνσμ}=0$ and the lowered Riemann tensor, as referenced in the module documentation to Wald Chapter 3 and MTW Chapter 13.
proof idea
This is a term-mode one-line wrapper that returns the hypothesis riemann_trace_vanishes_hypothesis unchanged to conclude the trace is zero. No additional lemmas or tactics are invoked beyond the assumption itself.
why it matters
The lemma supplies the vanishing trace required by ricci_minus_transpose_eq_trace and ricci_tensor_symmetric_thm to prove Ricci symmetry $R_{μν}=R_{νμ}$. It completes the algebraic step from the contracted Bianchi identity, ensuring consistency of the Einstein tensor. In the Recognition Science framework this supports the geometric layer of the forcing chain leading to $D=3$ spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.