MetricTensor
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not enforce symmetry of g or any index-raising properties.
- Does not compute the determinant or inverse metric components.
- Does not instantiate a concrete metric such as Minkowski or FLRW.
- Does not impose signature (3,1) or any curvature constraints.
formal statement (Lean)
18structure MetricTensor where
19 g : (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ := fun _ _ _ => 0
proof body
Definition body.
20
21/-- Local non-sealed bilinear form interface. -/
used by (40)
-
energy_conservation -
HamiltonianDensity -
hamiltonian_equivalence -
H_EnergyConservation -
H_HamiltonianEquivalence -
inverse_metric -
IsTimeTranslationInvariant -
metric_det -
StressEnergyTensor -
TotalHamiltonian -
metric_compatibility -
MetricTensor -
minkowski -
hilbert_variation_holds -
jacobi_variation -
jacobi_variation_structural -
einstein_symmetric -
einstein_tensor -
sourced_efe_coord -
vacuum_efe_coord -
contracted_bianchi -
efe_with_source -
perfect_fluid -
vacuum_is_special_case -
H_HomogenizationLimit -
homogenization_limit -
metric_det -
MetricTensor -
metric_FRW -
einstein_hilbert_action