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

MetricTensor

show as:
view Lean formalization →

MetricTensor supplies a minimal structure exposing only a determinant map from spacetime points to reals for the effective metric in homogenization arguments. Researchers deriving continuum limits from simplicial ledgers or constructing Hamiltonian densities cite this interface when abstracting the macroscopic g_mu nu. The declaration is a direct single-field structure definition that provides the det accessor without internal implementation.

claimA structure $M$ equipped with a determinant function $M.det : (x : Fin 4) → ℝ$ that returns the determinant of the local homogenized metric at each spacetime point $x$.

background

The Homogenization module proves existence of the continuum limit for simplicial ledger transitions, with the objective that the macroscopic metric $g_{μν}$ is the unique effective description of the underlying simplicial recognition density. Upstream MetricTensor structures in Hamiltonian, Gravity.Connection and Relativity.Geometry supply bilinear forms or symmetric component maps $g : Idx → Idx → ℝ$, while the meta version restricts to the determinant accessor alone. This local non-sealed interface supports scaffolding without committing to full metric axioms.

proof idea

One-line structure definition declaring the single det field of type (Fin 4 → ℝ) → ℝ.

why it matters in Recognition Science

The structure is required by energy_conservation, HamiltonianDensity, hamiltonian_equivalence and related hypotheses in Foundation.Hamiltonian, which use it to state time-translation invariance and small-deviation recovery of the standard Hamiltonian. It supplies the metric role inside the homogenization theorem, linking discrete recognition density to continuum physics and supporting the eight-tick octave and D = 3 spatial dimensions implicit in the 4D setup.

scope and limits

formal statement (Lean)

  17structure MetricTensor where
  18  det : (Fin 4 → ℝ) → ℝ
  19
  20/-- Determinant accessor for the local homogenization metric interface. -/

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.