MetricSmooth
plain-language theorem explainer
A metric tensor g at point x satisfies MetricSmooth when its components obey equality of mixed second partial derivatives for all index pairs. This condition is cited in derivations of the Riemann tensor trace vanishing and in antisymmetry proofs for the curvature tensor. The declaration is introduced directly as a definition that packages the Schwarz symmetry hypothesis on metric components.
Claim. A metric tensor $g$ at $x$ is smooth when, for all indices $a,b$, the mixed partial derivatives of the metric components commute: $∂_a ∂_b g_{μν}(x) = ∂_b ∂_a g_{μν}(x)$.
background
The module derives the standard algebraic symmetries of the Riemann tensor (antisymmetry in each pair, first Bianchi identity, pair exchange) from the Christoffel definition, following the strategy in Wald Chapter 3 and MTW Chapter 13. MetricTensor supplies the local bilinear form interface $g : (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ$. MetricSmooth encodes the hypothesis that mixed partials of these components are symmetric, which is the precise condition needed for the derivative terms in the Riemann trace to cancel.
proof idea
This is a definition that directly asserts the universal quantification ∀ a b, MixedPartialsSymmetric applied to the metric-component selector function at x. No lemmas or tactics are invoked; the declaration serves as a reusable hypothesis interface.
why it matters
It supplies the smoothness hypothesis required by riemann_trace_vanishes_of_smooth to conclude Σ_ρ R^ρ_ρμν = 0 and is referenced in riemann_antisymmetric_last_two. The definition closes the cancellation of mixed-partial terms in the Christoffel contraction, completing the algebraic route from antisymmetries plus the first Bianchi identity to pair exchange. Within the Recognition framework it anchors the geometric layer that supports curvature constructions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.