hasFDerivAt_HamDynN
plain-language theorem explainer
At every phase-space point the general-n dynamic Hamiltonian HamDynN(N) is Fréchet differentiable, with derivative exactly the continuous linear map HamDynND(N,x). Anyone computing Poisson brackets or partials of the lattice Hamiltonian cites this. The proof is a term-mode chain: unfold both sides and assemble the sum from coordinate Fréchet rules and product/sum calculus.
Claim. For every weight function $N:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and every point $x$ in the $n$-site phase space $(q,\pi)$, the map $x\mapsto H_N(x)=\sum_i (N_i/2)\bigl(\pi_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr)$ is Fréchet differentiable at $x$, and its derivative equals the continuous linear map $DH_N(x)$ written as the matching sum of kinetic and stiffness contributions.
background
The ambient space is the canonical lattice phase space: configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi$ on a periodic $n$-site ring (PhaseSpace n). Coordinate functionals $q_k$ and $\pi_k$ are continuous linear, so each has Fréchet derivative equal to itself (hasFDerivAt_coord_fst, hasFDerivAt_coord_snd).
HamDynN N is the exact general-$n$ shape of the two-site dynamic Hamiltonian: kinetic slot unweighted, stiffness slot weighted by the structure factor $g_j=1+q_j^2$. HamDynND N x is the candidate derivative, written so the metric-factor summand matches HasFDerivAt.const.add bookkeeping used for the $n=2$ model.
This module is Wave C2 R4 repair Step 2: lift DynamicStructureBracket.HamDyn and its self-bracket from $n=2$ to arbitrary $n$ with [NeZero n]. ZMod wraparound is periodic, so there is no boundary term.
proof idea
Term-mode proof. Unfold HamDynN and HamDynND, then apply HasFDerivAt.fun_sum over lattice sites. For each site $i$, build the summand derivative by composing:
hasFDerivAt_coord_snd itwice for the kinetic $\pi_i^2$ term;hasFDerivAt_const 1plushasFDerivAt_coord_fst itwice for the factor $1+q_i^2$;- difference of
hasFDerivAt_coord_fstat $i+1$ and $i$ for $(\Delta q_i)^2$; - product and sum rules, then scale by the constant $N_i/2$. No separate continuity or remainder argument: Mathlib's Fréchet calculus closes the identity with the pre-written linear map.
why it matters
This is the differentiability hinge for the general-$n$ dynamic structure bracket. Downstream, differentiable_HamDynN is the one-line wrapper (hasFDerivAt_HamDynN N x).differentiableAt. The momentum and configuration partials pderivP_HamDynN and pderivQ_HamDynN rewrite via .fderiv against HamDynND, yielding the kinetic slot $N_j\pi_j$ and the honest $\partial g/\partial q$ correction on the stiffness side.
Those partials feed the headline identity bracket (HamDynN N) (HamDynN M) whose RHS is the structure-factor form matching the $n=2$ case, and the recovery theorem bracket_HamDynN_recovers_bracket_HamDyn that specializes back to the concrete two-site inverse metric. In the Seven Gaps gravity stack this closes the Frechet bookkeeping needed before Kronecker collapse and periodic reindex of the dynamic structure function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.