H_HamiltonianEquivalence
plain-language theorem explainer
The definition H_HamiltonianEquivalence states that the recognition Hamiltonian density lies within ε³ of some standard Hamiltonian for all ε < 0.1. Researchers bridging recognition principles to classical field theory cite it to justify the reduction step before invoking energy conservation. It is introduced as a direct predicate definition that encodes the small-deviation condition without invoking further lemmas.
Claim. Let ψ be a recognition reality field and g a metric tensor. At point x the predicate holds when ∀ε < 0.1 there exists a standard Hamiltonian H_std such that |H_rec(ψ, g, x) − H_std(x)| < ε³, where H_rec is the Hamiltonian density obtained from the Legendre transform of the recognition Lagrangian.
background
The module derives the recognition Hamiltonian for the recognition reality field, an interface map (Fin 4 → ℝ) → ℝ. The metric tensor is a structure supplying local geometry components. Upstream the Hamiltonian density is defined via partialDeriv_v2 on the field, recovering the standard form ½(Π² + (∇Ψ)² + m²Ψ²) in the linear limit. This construction rests on the shifted cost H(x) = ½(x + x⁻¹) from CostAlgebra, which converts the recognition composition law into the d'Alembert equation.
proof idea
The declaration is a direct definition of the predicate as the quantified ε³ bound between HamiltonianDensity and an arbitrary standard Hamiltonian. No lemmas or tactics are applied; it functions as a one-line interface for the small-deviation regime.
why it matters
The predicate is invoked by the downstream theorem hamiltonian_equivalence to assert reduction of H_rec to the classical Hamiltonian in the ε << 1 regime. It supplies the bridge from the recognition formalism to energy conservation under time-translation invariance, aligning with the forcing chain from J-uniqueness through the phi-ladder. It leaves open the empirical test via Taylor expansion around the identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.