riemann_cert
plain-language theorem explainer
riemann_cert bundles the two core algebraic facts for the Riemann curvature tensor into a single certified object. Coordinate-based gravity calculations rely on it to invoke antisymmetry in the final index pair and automatic vanishing on flat backgrounds without separate derivations. The proof is a direct record construction that supplies the antisymmetric and flat_vanishes fields from the two dedicated lemmas.
Claim. The Riemann curvature tensor satisfies $R^ρ_{σμν} = -R^ρ_{σνμ}$ for all indices and equals zero whenever all Christoffel symbols and their first derivatives vanish identically.
background
The RiemannTensor module expresses the curvature tensor directly from Christoffel symbols Γ^ρ_μν and their partial derivatives. RiemannCert is the structure that packages the two algebraic facts required for later use: antisymmetry under swap of the last two indices together with vanishing on a flat background where every Γ and every dΓ is zero. These facts rest on the explicit coordinate definition of the tensor and on the upstream lemmas riemann_antisymmetric_last_two and riemann_flat_vanishes.
proof idea
The term proof constructs the RiemannCert record by assigning the antisymmetric field to the theorem riemann_antisymmetric_last_two and the flat_vanishes field to riemann_flat_vanishes. No tactics or additional reductions are performed; the proof is simply the record literal that populates the two required projections.
why it matters
This declaration supplies the certified RiemannCert object that encodes the minimal algebraic properties of the curvature tensor inside the Gravity section. It completes the local development of coordinate curvature and prepares the tensor for connection-based calculations. Within the Recognition framework it anchors the geometric side of the forcing chain by confirming that the standard Riemann symmetries hold in the chosen coordinate representation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.