MetricTensor
plain-language theorem explainer
A structure supplying a local non-sealed metric tensor interface for the Recognition Hamiltonian formalism, with g a placeholder map from pairs of 4-vectors and index selectors to reals that defaults to zero. Researchers deriving energy conservation for the RRF would cite this interface when instantiating the Hamiltonian density and Noether theorems. The definition is a one-line wrapper that provides the bilinear form stub required by downstream lemmas.
Claim. A metric tensor is a structure containing a function $g: (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ$ that defaults to the zero function, serving as a local non-sealed bilinear form on 4D spacetime.
background
The Recognition Hamiltonian Formalism module derives the Hamiltonian H_rec for the Recognition Reality Field (RRF) to prove energy conservation as a consequence of time-translation symmetry in the ledger. This MetricTensor supplies the required local metric interface, distinct from the symmetric-matrix version in Gravity.Connection, the determinant-only version in Meta.Homogenization, and the BilinearForm version in Relativity.Geometry.Metric. The module treats the metric as a non-sealed placeholder so that HamiltonianDensity and related constructions can proceed without fixing a concrete geometry.
proof idea
One-line wrapper that supplies the default zero function for the metric tensor components.
why it matters
This interface is used by energy_conservation (the Noether theorem asserting conservation of TotalHamiltonian under IsTimeTranslationInvariant), HamiltonianDensity (the Legendre transform recovering the standard ½(Π² + (∇Ψ)² + m²Ψ²) form), and hamiltonian_equivalence (the small-deviation reduction). It supplies the geometric scaffolding for the 4D spacetime in the Recognition Science Hamiltonian, consistent with the eight-tick octave and D = 3 spatial dimensions derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.