MetricTensor
plain-language theorem explainer
MetricTensor defines a symmetric real-valued map on four indices to represent metric components in local spacetime coordinates. Coordinate-based GR formalizations and Recognition Science Hamiltonian constructions cite this interface. It is supplied directly as a structure definition with an explicit symmetry field.
Claim. A metric tensor is a map $g : {0,1,2,3} × {0,1,2,3} → ℝ$ satisfying $g(μ,ν) = g(ν,μ)$ for all indices $μ,ν$.
background
The module works in coordinate patches to define the Levi-Civita connection and Christoffel symbols, avoiding Mathlib's missing abstract manifold support. Idx is the abbreviation Fin 4. Upstream MetricTensor structures appear in Foundation.Hamiltonian (local non-sealed bilinear form), Meta.Homogenization (determinant accessor), and Relativity.Geometry.Metric (BilinearForm version).
proof idea
The declaration is the structure definition itself; the symmetric field is part of the data.
why it matters
It supplies the metric input to energy_conservation, HamiltonianDensity, hamiltonian_equivalence, and related declarations in Foundation.Hamiltonian. The definition anchors the Gravity.Connection module's treatment of metric compatibility and Christoffel symmetry, supporting Recognition Science dynamics that require a coordinate metric for the Hamiltonian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.