pderivP_HamDynN
plain-language theorem explainer
The momentum partial of the general-n dynamic Hamiltonian HamDynN equals N_j p_j at every site. The structure factor g = 1 + q² multiplies only the stiffness slot, so it never enters the p-derivative. Anyone computing the Hamiltonian–Hamiltonian Poisson bracket on the n-site ring cites this identity. The proof evaluates the already-constructed Fréchet derivative on the pure-momentum basis vector and collapses the sum by Kronecker.
Claim. Let $N:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and let $x=(q,p)$ be a point of the $n$-site phase space. Write $H_N$ for the dynamic Hamiltonian whose $i$-th summand is $\frac{N_i}{2}\bigl(p_i^2 + (1+q_i^2)(q_{i+1}-q_i)^2\bigr)$. Then for every site $j$, $\partial H_N/\partial p_j = N_j\, p_j$.
background
The module generalizes the two-site dynamic structure bracket to arbitrary $n$ with wraparound on $\mathbb{Z}/n\mathbb{Z}$. Phase space is the product $(q,p)$ of two copies of $\mathbb{R}^{\mathbb{Z}/n\mathbb{Z}}$. The model Hamiltonian HamDynN keeps the kinetic slot unweighted and places the structure factor $g_j=1+q_j^2$ only on the discrete-gradient stiffness slot, matching the placement of the frozen weight in the earlier HamW model.
Partial derivatives are realized as Fréchet derivatives of real-valued maps on phase space, evaluated on the coordinate basis vectors. The upstream lemma hasFDerivAt_HamDynN supplies the continuous linear map HamDynND as the derivative of HamDynN at every point; that map is a sum over sites of scaled combinations of the coordinate functionals coordP and coordQ.
Because $g$ multiplies only the $q$-dependent stiffness term, the pure-momentum directional derivative should reduce to the elementary kinetic contribution $N_j p_j$. That is the content of the present identity.
proof idea
Rewrite the momentum partial as the Fréchet derivative of HamDynN applied to the pure-momentum basis vector $(0,e_j)$, using hasFDerivAt_HamDynN to replace the derivative by the explicit map HamDynND. Expand the continuous-linear-map sum. For each site $i$ a short algebraic computation (simp on Pi.single, then case-split on $i=j$ and ring) shows that the $i$-th summand evaluates to $(N_i p_i)\cdot\mathbf{1}_{i=j}$. The resulting finite sum collapses by the standard Kronecker identity sum_mul_ite to the single term $N_j p_j$.
why it matters
This is one of the two partial-derivative legs needed for the headline identity bracket_HamDynN_HamDynN, which states that the Poisson bracket of two dynamic Hamiltonians on the $n$-site ring equals
$\sum_j(N_j M_{j+1}-M_j N_{j+1}),(1+q_j^2),p_{j+1}(q_{j+1}-q_j)$.
That theorem simply unfolds the bracket definition and substitutes the present momentum partial together with the companion configuration partial. The same identity is reused by the recovery theorem that specializes $n=2$ and matches the earlier two-site bracket. In the Seven Gaps gravity program the calculation confirms that the $\partial g/\partial q$ corrections cancel inside the Hamiltonian–Hamiltonian bracket, so the dynamic structure factor does not spoil the algebraic form already known for frozen weights. It is a pure calculus step inside the Wave C2 R4 repair, not a new physical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.