HamDynN
plain-language theorem explainer
General-n dynamic Hamiltonian on the periodic lattice phase space: sum over sites of (lapse/2) times kinetic pi squared plus structure-weighted squared nearest-neighbor configuration jumps. Anyone proving the structure-function bracket or the Dirac continuum limit cites this model. Pure definitional lift of the two-site HamDyn formula to ZMod n.
Claim. For a lapse $N:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and phase-space point $(q,\pi)$ on the $n$-site periodic lattice, the dynamic Hamiltonian is $H_N(q,\pi)=\sum_i (N_i/2)\bigl(\pi_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr)$. Kinetic slot unweighted; stiffness carries structure factor $g_i=1+q_i^2$.
background
Phase space is the product of configuration and conjugate momentum on the cyclic lattice: pairs $(q,\pi)$ with both maps $\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. The two-site model already fixed the unfolded Hamiltonian used for Frechet calculus: each site contributes $(N_i/2)$ times kinetic $\pi_i^2$ plus a stiffness term weighted by $1+q_i^2$ on the squared jump $(q_{i+1}-q_i)^2$.
This module (Wave C2 R4 repair, Step 2) lifts that formula from $n=2$ to arbitrary $n$ with $\mathrm{NeZero},n$. ZMod wraparound is periodic, so there is no boundary term. The structure factor sits at the left split point of each bond, matching the placement used for background weights in the weighted Hamiltonian.
proof idea
Definitional body only: replace the fixed index type $\mathrm{ZMod},2$ by $\mathrm{ZMod},n$ and keep the same summand. No lemmas, no tactics. Consistency at $n=2$ is definitional equality with the original two-site Hamiltonian.
why it matters
Headline input to the general-$n$ dynamic structure-function identity: the Hamiltonian–Hamiltonian Poisson bracket collapses to a pure bond sum with factor $(N_j M_{j+1}-M_j N_{j+1})$ times $g_j,\pi_{j+1}(q_{j+1}-q_j)$, with $\partial g/\partial q$ corrections cancelling. Downstream continuum-binding theorems evaluate this bracket on sampled lapses and phase points, then take the scaled $n\to\infty$ limit to recover the continuum Dirac density for 1-periodic ContDiff-1 data. Also feeds the equivalent form written with the dynamic inverse metric and the recovery that $n=2$ matches the original two-site bracket.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.