TotalHamiltonian
plain-language theorem explainer
The TotalHamiltonian definition computes global recognition energy by summing the local density over a discrete 3D integer lattice of voxel centers, inserting time t into each coordinate and weighting by the metric volume element. Researchers deriving Noether theorems for the Recognition Reality Field cite this when establishing time-independent energy. The construction uses a Finset sum with a placeholder universal domain and multiplies each term by the square root of the absolute metric determinant.
Claim. Let $ψ$ be a recognition reality field and $g$ a metric tensor. The total Hamiltonian at time $t$ equals $∑_{ijk ∈ ℤ³} ℋ(ψ, g, x) √|det g(x)|$, where the four-vector $x$ sets its time component to $t$ and its spatial components to the integer triple $ijk$.
background
The module develops the Hamiltonian formalism for the Recognition Reality Field with the objective of proving energy conservation from time-translation symmetry in the ledger. The recognition reality field is an abbrev for maps from four-dimensional coordinates to the reals. The metric tensor is a structure supplying a bilinear form on those coordinates for volume computations. Upstream, the voxel is defined as the fundamental length quantum in RS-native units where the speed of light equals one.
proof idea
The definition declares spatial centers as a Finset of Fin 3 → ℤ triples. For each triple it builds the four-vector x by placing t in the time slot and the triple entries in the spatial slots. It then evaluates the Hamiltonian density at x, multiplies by the square root of the absolute metric determinant at x, and sums over the Finset.
why it matters
This definition supplies the total energy functional that enters the energy conservation theorem, which asserts constancy under time-translation invariance of the field and metric. It implements the spatial integral of the density required for the Noether argument in the Recognition Science ledger. The construction supports the hypothesis that total recognition energy remains constant for stationary sections of the potential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.