pderivQ_LocalHamFromProfile
plain-language theorem explainer
The Q-partial of a two-site local-profile Hamiltonian at coordinate k equals N_k times the cell-a derivative plus N_{k-1} times the neighboring cell-b derivative. Anyone computing Poisson brackets or the ham-ham form for n=2 local profiles cites this. The proof evaluates the already-established Fréchet derivative on the pure Q-direction and collapses the Z/2Z sum via indicator identities.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile with smooth partials $h_a,h_b,h_p$, and let $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. Write $H_N(x)=\sum_j N_j\, h(q_j,q_{j+1},p_j)$ on the $n=2$ phase space. Then for every site $k$ and every $x$, $\partial_{q_k} H_N(x)= N_k\, h_a(q_k,q_{k+1},p_k)+ N_{k-1}\, h_b(q_{k-1},q_k,p_{k-1})$.
background
Module groundwork for Wave C2 R5/R6: the local-profile functional equation at $n=2$ (mirroring HamDyn). A local profile is a map $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ evaluated on neighboring configuration coordinates and the on-site momentum. The assembled Hamiltonian is the weighted sum $H_N(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N_j, h(q_j,q_{j+1},p_j)$.
Smoothness is packaged as a structure supplying continuous partials $h_a,h_b,h_p$ together with a Fréchet derivative for each cell: the cell map differentiates as $h_a,\mathrm{d}q_j+h_b,\mathrm{d}q_{j+1}+h_p,\mathrm{d}p_j$. The linear map localCellD is exactly that combination of coordinate functionals, and LocalHamFromProfileD is the $N$-weighted sum of cells. Upstream, hasFDerivAt_LocalHamFromProfile already proves $H_N$ is Fréchet differentiable with that derivative; the private lemma cellD_qdir evaluates one cell on a pure $Q$-direction.
proof idea
Rewrite pderivQ as the Fréchet derivative of $H_N$ applied to $(\mathbf{e}k^Q,0)$, using hasFDerivAt_LocalHamFromProfile and unfolding LocalHamFromProfileD. The derivative is a sum of scaled cell maps; apply each to the pure $Q$-direction via cellD_qdir, which produces the two indicator terms $h_a\cdot\mathbf{1}{j=k}$ and $h_b\cdot\mathbf{1}_{j+1=k}$. Distribute the finite sum, collapse the two indicator sums with the standard sum_mul_ite lemmas, and use $k-1+1=k$ on $\mathbb{Z}/2\mathbb{Z}$ to rename the second index.
why it matters
Feeds directly into local_profile_ham_ham_form, which evaluates the Poisson bracket ${H_N,H_M}$ as a single cyclic sum of coefficients built from the profile partials. That bracket identity is the R6 attack surface for the local-profile functional equation: it reduces the dynamical ham-ham condition to the algebraic relation $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$. The module explicitly does not claim rigidity; this derivative lemma is the computational hinge that makes the reduction possible at $n=2$. In the broader SevenGaps gravity program it is scaffolding for matching hypersurface-deformation generators to recognition-native local Hamiltonians, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.