metric_det
plain-language theorem explainer
The metric determinant at a spacetime point is obtained by converting the bilinear metric form to its 4x4 matrix representation and computing the determinant of that matrix. Researchers deriving volume forms in emergent spacetime models or homogenization limits cite this accessor when normalizing densities. The implementation is a direct one-line wrapper delegating to the matrix conversion and standard determinant operation.
Claim. For a metric tensor given by a symmetric bilinear form on four-dimensional space, the determinant at coordinate point $x$ is the determinant of the $4$ by $4$ matrix obtained by evaluating the bilinear form on the standard basis vectors at $x$.
background
In the Relativity.Geometry.Metric module the metric tensor is a structure consisting of a bilinear form together with a symmetry condition that equates the form under a specific index swap on the last argument. This local interface supports coordinate-based calculations in four-dimensional spacetime and is imported by tensor and derivative modules. Upstream placeholders in the Hamiltonian module supply a trivial constant version of the same determinant while the Homogenization module defines an analogous accessor on its own metric structure for simplicial density calculations.
proof idea
The definition is a one-line wrapper that applies the metric_to_matrix conversion to obtain the 4x4 matrix representation of the bilinear form at the given point and then invokes the standard determinant operation on that matrix.
why it matters
This definition supplies the volume factor needed for the total Hamiltonian in the Foundation.Hamiltonian module and for the homogenization limit theorem that equates simplicial recognition density to the square root of the absolute metric determinant. It also appears in the spacetime emergence certificate establishing four-dimensional Lorentzian signature. In the Recognition Science framework it supports the transition from discrete recognition events to the continuous metric volume form, consistent with the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.