riemann_lowered_eq_explicit_hypothesis
plain-language theorem explainer
The declaration defines the hypothesis that the lowered Riemann tensor equals its explicit second-derivative expression involving metric derivatives and Christoffel symbols. General relativity calculations cite this to switch between abstract index-lowering and coordinate forms when proving symmetries. The definition is a direct equality statement with no computational steps or lemmas applied.
Claim. For a metric tensor $g$, spacetime point $x$, and indices $ρ,σ,μ,ν$, the lowered Riemann tensor $R_{ρσμν}$ equals the explicit form obtained by lowering the first index of the (1,3) Riemann tensor, which expands to second partial derivatives of the metric components plus quadratic Christoffel terms.
background
The RiemannSymmetries module derives algebraic properties of the Riemann curvature tensor from its definition via Christoffel symbols in local coordinates. The MetricTensor structure supplies the metric components as a bilinear form at each point $x$ in $ℝ^4$. The lowered Riemann tensor is obtained by contracting the first index of the (1,3) Riemann tensor with the metric to yield the fully covariant $R_{ρσμν}$.
proof idea
The declaration is a one-line definition that directly equates the lowered Riemann tensor to its explicit coordinate expression. No lemmas or tactics are invoked; the body simply names the equality as a hypothesis for later use.
why it matters
This hypothesis is invoked in downstream results such as riemann_lowered_antisym_first to establish antisymmetry in the first index pair and in curvature_axioms_hold to confirm the full curvature axioms. It supports the EndToEndChain that links the Recognition Composition Law through the Riemann tensor to the Einstein equations. The module cites Wald Section 3.2 for the explicit form, consistent with the framework requirement of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.