riemann_lowered_eq_explicit
plain-language theorem explainer
The theorem equates the lowered Riemann curvature tensor to its explicit coordinate expression once the defining hypothesis is granted. General relativists would cite it to unlock manifest antisymmetry when deriving index symmetries from the Christoffel connection. The proof is a one-line term that applies the hypothesis directly.
Claim. Let $g$ be a metric tensor on four-dimensional spacetime, $x$ a coordinate point, and $ρ,σ,μ,ν$ indices. Under the hypothesis $H(g,x,ρ,σ,μ,ν)$ that identifies the lowered Riemann tensor with its explicit form, $R_{ρσμν}(g,x)=R_{ρσμν}^{explicit}(g,x)$.
background
The module derives the standard algebraic symmetries of the Riemann curvature tensor from its definition via the metric connection. MetricTensor supplies the local symmetric bilinear form $g_{μν}$ at each spacetime point. The lowered Riemann tensor $R_{ρσμν}$ is the fully covariant version obtained by lowering one index on the curvature tensor built from Christoffel symbols and their derivatives. Upstream MetricTensor structures from the Hamiltonian and Gravity modules provide the non-sealed bilinear interface used throughout; the explicit curvature expressions live in the Curvature sibling module.
proof idea
The proof is a one-line term wrapper that applies the hypothesis h, which directly encodes the required equality between the abstract lowered Riemann tensor and its explicit coordinate formula.
why it matters
This equality supplies the bridge to the explicit form whose antisymmetry is immediate, feeding directly into riemann_lowered_antisym_first and ricci_tensor_symmetric_proof. It implements the first step of the module strategy that combines first-pair antisymmetry, second-pair antisymmetry, and the first Bianchi identity to obtain the pair-exchange symmetry $R_{ρσμν}=R_{μνρσ}$. The result aligns with the Wald reference cited in the module and supports the geometric layer of the Recognition Science forcing chain that fixes three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.