MetricSmooth
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert differentiability of the metric beyond second order.
- Does not impose any specific signature or coordinate form on g.
- Does not extend to non-coordinate bases without re-expression.
- Does not address global manifold topology or completeness.
Lean usage
theorem trace_example (g : MetricTensor) (x : Fin 4 → ℝ) (h : MetricSmooth g x) : riemann_trace_vanishes_of_smooth g x h _ := by sorryformal statement (Lean)
495def MetricSmooth (g : MetricTensor) (x : Fin 4 → ℝ) : Prop :=
proof body
Definition body.
496 ∀ a b, MixedPartialsSymmetric
497 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then a else b)) x
498
499/-! ## Trace Vanishing from Mixed Partial Symmetry
500
501The derivative part of Σ_ρ R^ρ_ρμν is:
502 Σ_ρ (∂_μ Γ^ρ_νρ - ∂_ν Γ^ρ_μρ)
503
504Using Γ^ρ_νρ = (1/2) g^{ρλ} (∂_ν g_{ρλ} + ∂_ρ g_{νλ} - ∂_λ g_{νρ})
505and the trace identity Σ_ρ Γ^ρ_νρ = ∂_ν(ln√|det g|),
506the derivative terms become ∂_μ∂_ν(ln√|det g|) - ∂_ν∂_μ(ln√|det g|) = 0
507by symmetry of mixed partials. -/
508
509/-- The Riemann trace vanishes for metrics with symmetric mixed partials.
510 Σ_ρ R^ρ_ρμν = 0 when ∂_μ∂_ν = ∂_ν∂_μ on metric components.
511
512 Proof structure:
513 1. Quadratic Christoffel terms vanish: already proved as
514 `christoffel_quadratic_trace_vanishes`
515 2. Derivative terms: Σ_ρ (∂_μ Γ^ρ_νρ - ∂_ν Γ^ρ_μρ)
516 The Christoffel contraction Σ_ρ Γ^ρ_αρ is a function of x only,
517 so its mixed partials commute by the Schwarz hypothesis. -/