HamiltonianDensity
The HamiltonianDensity definition supplies the recognition Hamiltonian density for the RRF field psi under metric g, expressed as half the squared norm of its spacetime derivatives at each point x. Field theorists deriving energy conservation from time-translation invariance in the Recognition Science ledger would cite this construction. The definition proceeds by direct summation of the squared partial derivatives using partialDeriv_v2 along the time axis and the three spatial directions.
claimThe recognition Hamiltonian density for the recognition reality field Ψ and metric tensor g at spacetime point x is given by $H_ {rec}(Ψ,g)(x) = ½[(∂₀Ψ(x))² + Σ_{i=1}^3 (∂_i Ψ(x))²]$.
background
The Recognition Reality Field (RRF) is the local non-sealed interface abbrev RRF := (Fin 4 → ℝ) → ℝ. The MetricTensor structure supplies a bilinear form g : (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ. This module derives the Hamiltonian for the RRF with the objective of proving energy conservation from time-translation symmetry in the ledger.
proof idea
This is a direct definition that constructs the density by evaluating the squared time derivative (partialDeriv_v2 psi 0 x) plus the sum over the three spatial directions (using i.succ for indices 1,2,3) of the squared spatial derivatives, then scaling by 1/2. It relies on the partialDeriv_v2 sibling definition for the derivative operator and Finset.sum for the spatial sum.
why it matters in Recognition Science
This definition provides the local energy density that feeds into TotalHamiltonian (the spatial integral over the cubic voxel lattice) and the hamiltonian_equivalence theorem, which shows reduction to the standard field Hamiltonian ½(Π² + (∇Ψ)² + m²Ψ²) for small deviations ε < 0.1. It advances the module goal of energy conservation from time-translation symmetry and connects to the J-cost via the linear-limit comment, supporting derivation of physical Hamiltonians from the Recognition Composition Law.
scope and limits
- Does not incorporate mass terms or interaction potentials.
- Does not depend on the metric g in its explicit computation.
- Does not include curvature effects from the metric.
- Does not account for the full Legendre transform involving conjugate momentum Π.
formal statement (Lean)
37noncomputable def HamiltonianDensity (psi : RRF) (g : MetricTensor) : (Fin 4 → ℝ) → ℝ :=
proof body
Definition body.
38 fun x =>
39 -- In the linear limit, the Hamiltonian density is proportional to the J-cost density.
40 -- For small variations, this recovers H ≈ ½(Π² + (∇Ψ)² + m²Ψ²).
41 (1/2 : ℝ) * (
42 (partialDeriv_v2 psi 0 x)^2 +
43 Finset.sum (Finset.univ : Finset (Fin 3)) (fun i => (partialDeriv_v2 psi (i.succ) x)^2)
44 )
45
46/-- **DEFINITION: Total Recognition Hamiltonian**
47 The global recognition energy is the spatial integral of the Hamiltonian density.
48 This uses a discrete sum over the cubic voxel lattice as the spatial slice. -/