christoffel_quadratic_trace_vanishes
plain-language theorem explainer
The quadratic terms involving products of Christoffel symbols cancel in the trace of the Riemann tensor. Workers in general relativity invoke this identity to simplify curvature traces. The argument equates the two summed expressions through reordering of finite sums and commutativity of multiplication.
Claim. For any metric tensor $g$, point $x$, and indices $μ,ν$, the double sum over $ρ,l$ of $(Γ^ρ_{μ l} Γ^l_{ν ρ} - Γ^ρ_{ν l} Γ^l_{μ ρ})$ equals zero, where $Γ$ are the Christoffel symbols of $g$.
background
The module proves algebraic symmetries of the Riemann tensor starting from its definition in Christoffel symbols. MetricTensor supplies a general bilinear form on Fin 4 without a concrete functional form. Christoffel symbols enter via the standard formula imported from the Euler-Lagrange action module. The lemma isolates the quadratic contributions inside the contracted Riemann expression, as sketched in the module's outline for trace vanishing.
proof idea
The tactic proof first proves the two double sums are identical. It applies Finset.sum_comm to reorder summation, then sum_congr with ring to match terms after index swap using commutativity of multiplication. The difference of the sums is then shown to be zero by substitution and simpa simplification.
why it matters
This lemma supplies the quadratic cancellation step inside riemann_trace_vanishes_of_smooth, which finishes the full trace identity under the MetricSmooth hypothesis. It completes the quadratic half of the standard result quoted from Wald, General Relativity, Section 3.2. In the Recognition framework it supports the geometric layer consistent with the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.