HamDynND
plain-language theorem explainer
Explicit Fréchet derivative of the general-n dynamic Hamiltonian (kinetic plus structure-weighted stiffness on the periodic lattice), returned as a continuous linear map on phase space. Lattice-gravity and SevenGaps workers cite it when extracting momentum or configuration partials and when forming the dynamic structure Poisson bracket. The body is a term-by-term differentiated sum of scaled coordinate functionals, with a deliberate 0+ placeholder matching the const-add rule used for the metric factor.
Claim. For a site-dependent multiplier $N:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and a phase-space point $x=(q,\pi)$ on the $n$-site periodic lattice, the continuous linear map $DH_N(x):T_x\mathrm{PhaseSpace}_n\to\mathbb{R}$ is the candidate Fréchet derivative of the dynamic Hamiltonian $H_N(x)=\sum_i(N_i/2)\bigl(\pi_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr)$.
background
The module repairs Wave C2 R4 Step 2 by lifting the two-site dynamic structure bracket to arbitrary $n$ with $\mathrm{NeZero},n$. Phase space is the product of configuration and conjugate-momentum fields $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ on the periodic lattice; coordinate functionals $\mathrm{coordQ},i$ and $\mathrm{coordP},i$ extract the $i$-th slots as continuous linear maps.
The underlying energy $H_N$ (sibling HamDynN) places an unweighted kinetic slot $\pi_i^2$ and a stiffness slot carrying the structure factor $g_i=1+q_i^2$ on the discrete gradient $(q_{i+1}-q_i)^2$, scaled by the lapse $N_i/2$. At $n=2$ this is definitionally the older two-site dynamic Hamiltonian.
This declaration packages the candidate derivative so that a later HasFDerivAt lemma can certify it by summing elementary product and chain rules, reusing the same Frechet bookkeeping pattern as the two-site HamDynD.
proof idea
Definitional construction, not a proved theorem. Each summand of $H_N$ is differentiated by hand into continuous linear maps: the kinetic piece contributes two copies of $\pi_i,\mathrm{coordP},i$; the stiffness piece applies the product rule to $g_i(\Delta q_i)^2$, with the constant-$1$ part of $g$ producing a pure $\Delta q$ factor and the $q_i^2$ part producing both a $\Delta q$ factor and a $0+2q_i,\mathrm{coordQ},i$ correction (the leading $0$ matches HasFDerivAt.const.add from the metric factor, same convention as the two-site derivative). Every piece is scaled by $N_i/2$ and summed over $\mathbb{Z}/n\mathbb{Z}$.
why it matters
Required witness for hasFDerivAt_HamDynN, which asserts that this map is the true Fréchet derivative of the general-$n$ dynamic Hamiltonian. That lemma unlocks the momentum partial (kinetic slot unchanged by $g$) and the honest configuration partial (frozen background-weight contribution plus the $\partial g/\partial q$ correction $N_j q_j(\Delta q_j)^2$).
Those partials feed the general-$n$ Poisson bracket identity ${H_N,H_M}x=\sum_j(N_j M{j+1}-M_j N_{j+1})\cdot((1+q_j^2)\pi_{j+1}(q_{j+1}-q_j))$, the true RHS derived from the calculus and matching the $n=2$ case. The structure factor sits at the left split point, same placement as the background weight in the static Hamiltonian. This closes the $n=2$ restriction in the SevenGaps dynamic-structure stack for lattice hypersurface deformation; ZMod wraparound is periodic, so there is no boundary term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.