riemann_trace_vanishes_hypothesis
plain-language theorem explainer
The declaration posits that the contraction of the Riemann tensor over its first two indices vanishes identically. Researchers closing the discrete-to-continuum bridge from the Recognition Composition Law to the Einstein equations would cite it when establishing Ricci symmetry. It is introduced as a direct equality hypothesis whose discharge later relies on torsion freedom and metric compatibility of the Levi-Civita connection.
Claim. Let $g$ be a metric tensor and $x$ a spacetime point. Then the trace contraction satisfies $R^ρ{}_{ρμν}(g,x)=0$ for all indices $μ,ν$.
background
The module derives algebraic symmetries of the Riemann tensor from its expression in Christoffel symbols of a metric. MetricTensor is the structure supplying the symmetric bilinear form $g_{αβ}(x)$ at each point, appearing in multiple imported modules as a local non-sealed interface. The sibling definition riemann_trace computes the explicit sum $∑ρ R^ρ{}{ρμν}$ by contracting the Riemann tensor over the repeated index.
proof idea
The declaration is a one-line definition that packages the equality riemann_trace g x μ ν = 0 as a Prop. It functions as a hypothesis interface rather than an internal proof; downstream theorems such as ricci_tensor_symmetric_thm simply apply the supplied hypothesis directly.
why it matters
This hypothesis is required by curvature_axioms_hold and ricci_tensor_symmetric_thm, which in turn supply the CurvatureAxiomsHold field inside the EndToEndChain structure. That structure records the proved path from the Recognition Composition Law through J-uniqueness, the forced φ, D=3, the eight-tick octave, and the Minkowski metric to the Einstein equations. The doc-comment notes that full discharge needs symmetry of mixed partials and cites Wald Section 3.2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.