metric_to_matrix_symmetric
plain-language theorem explainer
The lemma shows that the 4x4 matrix extracted from any metric tensor at a spacetime point x is symmetric. It is invoked when converting abstract tensors to coordinate matrices for curvature or inverse-metric calculations. The proof reduces the claim to entrywise equality by matrix extensionality and applies the built-in symmetry axiom of the metric tensor on swapped lower-index selectors.
Claim. Let $g$ be a metric tensor and $x : Fin 4 → ℝ$. Let $M$ be the matrix whose entries are given by the bilinear form $g(x, 0, λ_{ij})$ where $λ_{ij}(0) = i$ and $λ_{ij}(1) = j$. Then $M^T = M$.
background
In Relativity.Geometry.Metric the metric tensor is a structure MetricTensor whose field g is a bilinear form and whose field symmetric asserts that g x up low equals g x up after swapping the two lower indices via the selector (fun i => if i.val = 0 then low 1 else low 0). This local interface is imported from Foundation.Hamiltonian.MetricTensor and Gravity.Connection.MetricTensor, both of which treat the metric as a symmetric bilinear object on four spacetime indices. The sibling function metric_to_matrix converts the abstract form into an explicit matrix at each point x.
proof idea
The term proof begins with matrix extensionality (ext i j). It unfolds metric_to_matrix and Matrix.transpose, then applies the symmetric axiom of g at the zero upper index and the swapped lower-index selector. Simplification of the Fin.val conditionals (one_ne_zero, ite_true, ite_false) yields the required entry equality.
why it matters
The result guarantees that every coordinate matrix representation inherits the symmetry required by the metric tensor axiom, a prerequisite for the inverse_metric and metric_det siblings in the same module. It directly supports the standard assumption used in derivations of the Levi-Civita connection and Einstein tensor within the Recognition framework's relativity layer. No downstream uses are recorded, indicating it functions as an internal consistency lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.