pith. machine review for the scientific record. sign in
structure definition def or abbrev high

MetricTensor

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  39structure MetricTensor where
  40  g : Idx → Idx → ℝ
  41  symmetric : ∀ mu nu, g mu nu = g nu mu
  42
  43/-- The inverse metric g^{mu nu} (satisfying g^{mu rho} g_{rho nu} = delta^mu_nu). -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.