riemann_lowered_explicit_antisym_first
plain-language theorem explainer
The explicit lowered Riemann tensor satisfies antisymmetry under exchange of the first two indices. Relativists and Recognition Science curvature derivations cite it to anchor the first pair antisymmetry before chaining to pair exchange. The proof unfolds the explicit definition, records metric symmetry, commutes and negates the double sum over quadratic Christoffel terms while relabeling indices, and combines the negated derivative and quadratic pieces with linear arithmetic.
Claim. Let $R^E_{ρσμν}$ denote the explicit lowered Riemann tensor built from second partial derivatives of the metric $g$ together with quadratic terms in its Christoffel symbols. Then $R^E_{ρσμν} = -R^E_{σρμν}$ holds for all indices $ρ,σ,μ,ν$.
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 symmetric bilinear form $g_{αβ}(x)$. The explicit lowered form expands the standard expression containing second derivatives of metric components plus quadratic Christoffel contributions. Upstream results include the Christoffel symbol construction and the metric symmetry property $g_{αβ}=g_{βα}$ used in every relabeling step.
proof idea
Unfold the explicit definition. Record metric symmetry from the MetricTensor interface. For the quadratic sum, commute the double Finset sum, distribute negation, apply sum_congr with metric symmetry after index relabeling, and simplify with ring. The second-derivative block negates by direct index swap. Combine both negated blocks with linarith.
why it matters
This supplies the explicit antisymmetry invoked by the downstream theorem riemann_lowered_antisym_first once the explicit-equivalence hypothesis is assumed, completing one of the three pillars (first-pair antisymmetry, second-pair antisymmetry, first Bianchi) that yield pair exchange in the module. The construction sits inside the Recognition Science relativity layer whose metric originates from the phi-ladder forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.