minkowski_riemann_zero
plain-language theorem explainer
The Riemann curvature tensor vanishes identically when constructed from the Minkowski metric. Researchers deriving flat-space limits or verifying discrete-to-continuum bridges in gravity would cite this result. The proof is a direct tactic reduction that substitutes the vanishing Christoffel symbols and their zero derivatives into the standard Riemann expression and simplifies.
Claim. For the Minkowski metric tensor, the Riemann curvature tensor satisfies $R^ρ{}_{σμν}(x)=0$ at every point $x∈ℝ^4$, for the indicated index placements.
background
The module constructs Christoffel symbols from a given metric tensor via the standard formula involving partial derivatives of the metric components. The Riemann tensor is defined by the usual coordinate expression involving first derivatives of the Christoffel symbols together with quadratic products of the symbols themselves. The Minkowski metric is constant, so its Christoffel symbols are identically zero; the auxiliary lemma minkowski_christoffel_zero_proper records this fact. Upstream, partialDeriv_v2 supplies the directional derivative along coordinate rays, and partialDeriv_v2_const records that constants have vanishing derivatives.
proof idea
The tactic proof first unfolds the definition of riemann_tensor. It then asserts that all Christoffel symbols built from minkowski_tensor vanish, citing minkowski_christoffel_zero_proper. A second fact records that partialDeriv_v2 of any constant-zero function is zero, via partialDeriv_v2_const. The final simp step substitutes these facts and reduces the entire expression, including the sum over repeated indices, to zero.
why it matters
This theorem supplies the curvature-vanishing step required by minkowski_ricci_zero and by flat_chain_holds in DiscreteBridge, which assembles the complete flat-chain record. It confirms that the Recognition framework recovers the expected zero curvature of Minkowski space, consistent with the forcing chain that fixes D=3 spatial dimensions and the constant metric case of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.