MetricTensor
plain-language theorem explainer
This structure supplies a minimal determinant accessor for the local metric in the homogenization scaffolding. Workers on the continuum limit of simplicial ledgers cite it when passing metric data into Hamiltonian constructions. The declaration is a direct structure definition exposing only the det field on 4-tuples of reals.
Claim. A local metric interface consists of a structure equipped with a determinant map $det : (Fin 4 → ℝ) → ℝ$.
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. This MetricTensor is the non-sealed interface used inside that scaffolding. Upstream, Foundation.Hamiltonian.MetricTensor supplies a local non-sealed bilinear form interface, Gravity.Connection.MetricTensor defines a symmetric 4x4 matrix at each point, and Relativity.Geometry.Metric.MetricTensor equips a bilinear form with an explicit symmetry axiom.
proof idea
One-line structure definition that introduces the det accessor.
why it matters
The structure feeds the Hamiltonian module theorems energy_conservation, hamiltonian_equivalence and the definitions HamiltonianDensity and H_EnergyConservation. It supplies the metric handle required by the homogenization theorem to extract the continuum metric from the simplicial ledger. The declaration sits inside the meta layer that bridges Recognition Science forcing chain steps to macroscopic geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.