riemann_pair_exchange_from_definition
plain-language theorem explainer
The declaration establishes that the pair-exchange symmetry for the lowered Riemann tensor holds whenever the lowered components match their explicit expression. General relativists deriving curvature identities from the Christoffel definition would cite this result to replace an axiom with a theorem. The proof is a one-line wrapper that invokes the dedicated exchange lemma under the supplied hypothesis.
Claim. Let $g$ be a metric tensor and $x$ a spacetime point. Under the hypothesis that the lowered Riemann tensor equals its explicit component form for all index combinations, the identity holds: $$g(x)(e_0, e_0) R^0{}_{0 0 0} + g(x)(e_0, e_1) R^1{}_{0 0 0} + g(x)(e_0, e_2) R^2{}_{0 0 0} + g(x)(e_0, e_3) R^3{}_{0 0 0} = g(x)(e_0, e_0) R^0{}_{0 0 0} + g(x)(e_0, e_1) R^1{}_{0 0 0} + g(x)(e_0, e_2) R^2{}_{0 0 0} + g(x)(e_0, e_3) R^3{}_{0 0 0}$$ (with the second sum obtained by exchanging the first and third index pairs in the standard lowered convention).
background
The module derives the algebraic symmetries of the Riemann curvature tensor directly from its definition in terms of Christoffel symbols. MetricTensor supplies the local symmetric bilinear form $g$ at each point $x$ in four-dimensional spacetime. The riemann_tensor function returns the components $R^ρ{}_{σμν}$ via the standard expression involving first partial derivatives of the Christoffel symbols plus the quadratic connection terms, as given in the Gravity.RiemannTensor module.
proof idea
The proof is a one-line wrapper that applies the lemma riemann_pair_exchange_proof to the supplied metric, point, indices, and explicit-form hypothesis.
why it matters
This result supplies the explicit-form version of the pair-exchange symmetry $R_{ρσμν}=R_{μνρσ}$ that the module identifies as the central step completing the curvature axioms. It is invoked by the antisymmetry theorem for the last two indices in the same file. Within the Recognition framework it closes the derivation of standard Riemann properties from the explicit definition, feeding the Ricci symmetry and the Einstein tensor construction while remaining inside the four-dimensional forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.