MetricTensor
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.