MetricTensor
plain-language theorem explainer
The MetricTensor structure equips a bilinear form on four-dimensional vectors with symmetry under interchange of its two lower indices. Researchers deriving energy conservation or Hamiltonian equivalence in the Recognition framework cite it when passing a metric to the Hamiltonian density. The extensionality lemma follows from a direct case split on the two structures and simplification.
Claim. A metric tensor is a pair consisting of a bilinear form $g: (ℝ^4 → ℝ) × (ℝ^4 → ℝ) × ({0,1} → ℝ^4) → ℝ$ together with the symmetry condition $g(x,u,l) = g(x,u,l')$ where $l'$ is obtained by swapping the two components of $l$.
background
BilinearForm is the local interface abbrev (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ introduced in the Hamiltonian module. The present structure augments this interface with an explicit symmetry requirement on the lower pair of indices. Parallel metric structures appear upstream in Gravity.Connection (symmetric 4×4 matrix with g(μ,ν)=g(ν,μ)) and in Meta.Homogenization (determinant accessor only).
proof idea
The structure itself is introduced by direct definition. Its extensionality lemma is proved by case analysis on the two arguments followed by simp_all.
why it matters
MetricTensor supplies the metric type required by the Hamiltonian module for energy_conservation, HamiltonianDensity, and hamiltonian_equivalence. It thereby links the relativity geometry layer to the claim that recognition energy is conserved under time-translation invariance and reduces to the standard Hamiltonian in the small-deviation regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.