MetricTensor
plain-language theorem explainer
A structure supplying the components of a symmetric bilinear form g on four indices, representing the metric tensor in a local coordinate patch. Hamiltonian and connection computations in the Recognition framework cite it when passing metric data into energy densities or Christoffel symbols. The declaration is a direct structure definition whose two fields encode the map and the symmetry condition with no further reduction.
Claim. A metric tensor is a map $g : I × I → ℝ$ on the index set $I = {0,1,2,3}$ together with the axiom $g(μ,ν) = g(ν,μ)$ for all indices $μ,ν$.
background
The module works in a coordinate patch on 4-dimensional spacetime, avoiding abstract manifold machinery. Idx is the abbreviation Fin 4, so the indices label the four coordinates. The structure therefore supplies the symmetric components $g_{μν}$ that appear in all subsequent Christoffel and Hamiltonian expressions.
proof idea
Structure definition. The two fields directly record the component map and the symmetry requirement; no lemmas or tactics are applied.
why it matters
Supplies the metric data required by the Hamiltonian theorems energy_conservation and hamiltonian_equivalence in Foundation.Hamiltonian. It anchors the local geometry inside the Levi-Civita formalization, enabling the Christoffel symbols that connect to curvature and dynamics. In the Recognition framework it provides the concrete interface between the J-cost and the eight-tick spacetime geometry used for the D=3 spatial derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.