riemann_lowered_pair_exchange
plain-language theorem explainer
The lowered Riemann curvature tensor satisfies the pair exchange R_ρσμν = R_μνρσ when the metric obeys the explicit-form hypothesis. General relativists and Recognition Science modelers cite this to confirm curvature axioms for their metrics. The proof derives the equality algebraically by cycling the first Bianchi identity four times, invoking both antisymmetries, and closing with linear arithmetic.
Claim. Let $g$ be a metric tensor and $x$ a spacetime point. If the explicit hypothesis holds for all index tuples, then the lowered Riemann tensor obeys $R_{ρσμν}(g,x) = R_{μνρσ}(g,x)$.
background
The module derives the algebraic symmetries of the Riemann curvature tensor from its Christoffel-symbol definition in four-dimensional spacetime. MetricTensor supplies the local bilinear form used to lower indices, while riemann_lowered denotes the fully covariant version R_ρσμν. The first Bianchi identity riemann_lowered_first_bianchi states R_ρσμν + R_ρμνσ + R_ρνσμ = 0, and the antisymmetry lemmas supply R_ρσμν = -R_σρμν together with antisymmetry in the final pair.
proof idea
Four instances of riemann_lowered_first_bianchi are obtained by cycling the indices to (ρ,σ,μ,ν), (σ,ρ,μ,ν), (μ,ν,ρ,σ) and (ν,μ,ρ,σ). Antisymmetry in the last pair is taken from riemann_lowered_antisym_last; antisymmetry in the first pair is taken from riemann_lowered_antisym_first under the explicit hypothesis. These identities are passed to linarith, which executes the combination (A)+(B)-(C)-(D) to produce the factor-of-four equality.
why it matters
The result supplies the pair-exchange property required by curvature_axioms_hold, which verifies that both curvature axioms hold as theorems once the explicit and trace-vanishing hypotheses are met. It also discharges riemann_pair_exchange_proof, matching the signature of the original axiom. Within the Recognition framework the identity closes the geometric verification step that supports the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.