RiemannCert
plain-language theorem explainer
RiemannCert bundles the antisymmetry of the Riemann curvature tensor in its final index pair together with its automatic vanishing when the connection is identically zero. Coordinate-based gravity calculations cite it to confirm that any explicit expression for R satisfies these minimal algebraic checks. The structure is realized by direct field assignment to two prior lemmas on antisymmetry and flat vanishing.
Claim. The structure RiemannCert asserts that the Riemann tensor satisfies $R^ρ_{σμν}=-R^ρ_{σνμ}$ for arbitrary Christoffel symbols Γ and their derivatives, and that $R^ρ_{σμν}=0$ identically whenever both Γ and its derivatives vanish.
background
The module expresses the Riemann curvature tensor in local coordinates from Christoffel symbols γ and first derivatives dγ via the standard combination of partial derivatives and quadratic connection terms. It records the algebraic symmetries that follow immediately from this expression. The setting is coordinate general relativity; no metric or torsion-free assumption is imposed beyond the explicit formulas.
proof idea
The structure is defined by assigning its antisymmetric field to the lemma establishing antisymmetry in the last two indices and its flat_vanishes field to the lemma showing vanishing for the zero connection. No further steps are performed.
why it matters
The structure is instantiated by the theorem riemann_cert that packages the two properties for use in the gravity module. It supplies the basic algebraic certification required before invoking the algebraic Bianchi identity or proceeding to curvature-derived quantities in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.