metric_det
plain-language theorem explainer
The metric_det definition supplies the constant value 1 as a stand-in for the determinant of the metric tensor inside the Recognition Hamiltonian module. Workers on the Recognition Reality Field cite it when constructing the total energy integral or homogenization limits. The implementation is a direct constant return that discards both the metric argument and the evaluation point.
Claim. For any metric tensor interface $g$ and point $x : Fin 4 → ℝ$, the determinant is defined by $det(g,x) := 1$.
background
The module derives the Hamiltonian for the Recognition Reality Field with the objective of proving energy conservation from time-translation symmetry. MetricTensor is the local non-sealed interface given by a structure whose g component maps a point, two index vectors, and a 2-tuple of indices to a real number, defaulting to zero. Upstream metric_det definitions appear in Relativity.Geometry.Metric as the determinant of the matrix representation and in Meta.Homogenization as direct access to a det field on the local metric structure.
proof idea
One-line definition that returns the constant 1.
why it matters
The definition is referenced by TotalHamiltonian, which forms the global recognition energy by summing the density over cubic voxels, and by the homogenization limit theorem that equates simplicial density to the square root of the absolute metric determinant. It also appears in the spacetime emergence certificate. The placeholder supports the transition from the Recognition Composition Law to a concrete Hamiltonian while the full metric components remain under development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.