CurvatureAxiomsHold
plain-language theorem explainer
CurvatureAxiomsHold bundles the pair-exchange symmetry of the lowered Riemann tensor with the symmetry of the Ricci tensor for a given metric tensor g at point x. Workers closing the discrete-to-continuum bridge cite this structure when verifying curvature axioms under explicit-form and trace-vanishing hypotheses. It is realized as a Prop structure whose fields are populated by separate symmetry theorems derived from the Christoffel definition of the Riemann tensor.
Claim. For a metric tensor $g$ and point $x$, the lowered Riemann tensor satisfies $R_{ρσμν}(g,x)=R_{μνρσ}(g,x)$ for all indices $ρ,σ,μ,ν$, and the Ricci tensor is symmetric: $R_{μν}(g,x)=R_{νμ}(g,x)$.
background
The module proves symmetry properties of the Riemann curvature tensor from its definition via Christoffel symbols. Key objects include the lowered Riemann tensor (fully covariant $R_{ρσμν}$) and the Ricci tensor obtained by contraction $R_{μν}=∑ρ R^ρ{μρν}$. Upstream MetricTensor supplies the local symmetric bilinear form on Fin 4 indices, while ricci_tensor performs the indicated contraction. The local setting assumes smooth metrics obeying the explicit-form and trace-vanishing hypotheses referenced in the module strategy.
proof idea
The declaration is a structure definition that collects two independent results. The pair_exchange field is supplied by the algebraic identity riemann_lowered_pair_exchange, which combines first-pair antisymmetry, second-pair antisymmetry, and the first Bianchi identity. The ricci_symmetric field is supplied by ricci_tensor_symmetric_proof under the trace-vanishing hypothesis.
why it matters
This structure closes the curvature-axioms step inside the end-to-end chain that runs from the Recognition Composition Law through J-uniqueness, the forced phi fixed point, D=3, the eight-tick octave, and the Minkowski metric to the Einstein equations. It is referenced by EndToEndChain, which records what is proved versus hypothesized in the discrete-continuum bridge. The constructing theorem curvature_axioms_hold instantiates the structure once the explicit-form and trace-vanishing hypotheses are supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.