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

MetricTensor

show as:
view Lean formalization →

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.

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

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.

scope and limits

formal statement (Lean)

  11structure MetricTensor where
  12  g : BilinearForm
  13  symmetric : ∀ x up low, g x up low = g x up (fun i => if (i : ℕ) = 0 then low 1 else low 0)
  14
  15@[ext]
  16lemma MetricTensor.ext (g1 g2 : MetricTensor) (h : g1.g = g2.g) : g1 = g2 := by

proof body

Definition body.

  17  cases g1; cases g2; simp_all
  18

used by (40)

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

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.