MixedPartialsSymmetric
Mixed partial symmetry states that second derivatives of a scalar function on four-dimensional space commute in their indices. General relativists cite it when assuming coordinate smoothness for curvature computations in the Riemann tensor. The declaration is a direct definition that equates the two orders of the secondDeriv operator without additional steps.
claimFor a scalar function $f: (Fin 4 → ℝ) → ℝ$ and point $x ∈ Fin 4 → ℝ$, the second partial derivatives satisfy $∂_μ ∂_ν f(x) = ∂_ν ∂_μ f(x)$ for all indices $μ, ν$.
background
The RiemannSymmetries module derives algebraic identities for the Riemann curvature tensor from Christoffel symbols of a metric tensor. The secondDeriv operator, imported from the Derivatives module, computes iterated directional derivatives $∂_μ ∂_ν f$ by differentiating along coordinate rays. This definition encodes the classical commutativity of mixed partials (Schwarz theorem) specialized to four dimensions and the functions appearing in metric components.
proof idea
The declaration is a definition that directly equates secondDeriv f μ ν x with secondDeriv f ν μ x for all μ ν. It functions as a one-line wrapper that applies the secondDeriv operator in both orders and asserts their equality.
why it matters in Recognition Science
This definition is required by the downstream MetricSmooth property, which ensures the metric tensor components admit symmetric mixed partials before the Riemann tensor symmetries (antisymmetry in first pair, first Bianchi identity, pair exchange) are derived. It supplies the smoothness hypothesis referenced in the module strategy that leads to R_ρσμν = R_μνρσ. In the broader framework it anchors the geometric layer used to reach D = 3 from the forcing chain.
scope and limits
- Does not prove the commutativity of mixed partials; it defines the property.
- Does not guarantee that second derivatives exist for arbitrary f.
- Does not extend beyond four-dimensional coordinate charts.
- Does not constrain higher-order derivatives or non-scalar fields.
formal statement (Lean)
491def MixedPartialsSymmetric (f : (Fin 4 → ℝ) → ℝ) (x : Fin 4 → ℝ) : Prop :=
proof body
Definition body.
492 ∀ μ ν, secondDeriv f μ ν x = secondDeriv f ν μ x
493
494/-- A metric whose components have symmetric mixed partials everywhere. -/