H_EnergyConservation
plain-language theorem explainer
The definition encodes the property that total recognition energy stays constant in time whenever the recognition reality field and metric tensor are invariant under time translations. Researchers deriving Noether-type conservation laws from ledger symmetries would cite it when assuming time-translation invariance. It directly packages the implication as a Prop without further reduction steps.
Claim. Let $ψ$ be the recognition reality field and $g$ a metric tensor. The predicate $H(ψ,g)$ holds precisely when time-translation invariance of $ψ$ and $g$ implies that the total Hamiltonian equals its value at the initial time for every later time $t$.
background
The Recognition Hamiltonian Formalism module constructs the Hamiltonian for the Recognition Reality Field (RRF), an abbrev for maps from four-dimensional coordinates to reals. The metric tensor is a structure supplying a bilinear form on these coordinates. TotalHamiltonian sums the local density over a cubic lattice of spatial centers, with time as the zeroth coordinate, yielding the global recognition energy.
proof idea
This is a direct definition that packages the conservation statement as the logical implication from IsTimeTranslationInvariant to constancy of TotalHamiltonian. No lemmas are applied; the body is the implication itself.
why it matters
It supplies the hypothesis used by the downstream energy_conservation theorem, which asserts that time-translation invariance forces conservation of total recognition energy. The module objective is to obtain energy conservation from time-translation symmetry in the ledger, placing the result inside the Recognition Science derivation of conserved quantities from symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Neural networks gain continuous depth by solving ODEs
"the adjoint sensitivity method (Pontryagin et al., 1962). This approach computes gradients by solving a second, augmented ODE backwards in time"