HamDyn
plain-language theorem explainer
Two-site dynamic Hamiltonian on the lattice phase space, weighted by a lapse field N. It pairs kinetic momentum squares with a configuration-dependent discrete gradient term coming from the concrete dynamic inverse metric. Downstream R1 proofs cite it as the honest Frechet-ready Hamiltonian whose bracket recovers the dynamic structure function. The body is an explicit finite sum, written unfolded for termwise differentiation.
Claim. For a lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,\pi)$ on the two-site periodic lattice, define $$H_{\mathrm{dyn}}(N,x)=\sum_{i\in\mathbb{Z}/2\mathbb{Z}}\frac{N_i}{2}\Bigl(\pi_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\Bigr).$$
background
The ambient setting is Wave C2 residual work on the dynamic structure-function bracket at two lattice sites. Phase space is the product of configuration and conjugate momentum maps on the periodic lattice: $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, specialized here to $n=2$.
The module targets residuals R0 and R1 from the QG Wave C2 gap draft. R0 records that naively plugging a configuration-dependent metric factor into a frozen Hamiltonian slot and reusing frozen partials fails: the $q$-partial picks up an uncompensated $\partial g/\partial q$ term. R1 requires an honest Frechet derivative of a candidate Hamiltonian that still lands in the phase-space-dependent Hamiltonian construction for the concrete dynamic inverse metric.
This definition is the unfolded scalar Hamiltonian used for that calculus. The factor $(1+q_i^2)$ is the on-site dynamic inverse-metric weight; the squared nearest-neighbour difference is the discrete spatial gradient on $\mathbb{Z}/2\mathbb{Z}$.
proof idea
Definition by explicit finite sum, not a derived theorem. For each site $i\in\mathbb{Z}/2\mathbb{Z}$ one multiplies the lapse weight $N_i/2$ by the sum of $\pi_i^2$ and the metric-weighted squared hop $(1+q_i^2)(q_{i+1}-q_i)^2$, then sums over the two sites. The expansion is deliberately unfactored so later Frechet and partial-derivative lemmas can differentiate term by term without unfolding nested helpers. Equality with the naive dynamic Hamiltonian wrapper is a separate one-line ring identity.
why it matters
This is the working Hamiltonian of the R1 closure on two sites. It is the ham field of the concrete phase-space-dependent Hamiltonian construction for the dynamic inverse metric, and it is the object whose Hamiltonian–Hamiltonian bracket is proved equal to the target dynamic structure function (the R1 headline identity). Continuum Dirac-algebra work reuses the same shape identity when controlling wronskian-type errors in the lattice-to-continuum limit.
Within the Seven Gaps gravity stack it supplies the dynamic, configuration-dependent side of the hypersurface-deformation algebra at the smallest nontrivial lattice. It does not close gap-5 constraint recovery; continuum and HKT residuals stay open. Relative to the broader Recognition forcing chain it is local scaffolding for the gravitational sector, not a T0–T8 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.