pderivP_LocalHamFromProfile
plain-language theorem explainer
The momentum partial of a two-site local-profile Hamiltonian equals the site weight times the profile's own p-partial at that site. Anyone computing Poisson brackets or kinetic regularity for n=2 HKT local profiles cites this identity. The proof evaluates the Fréchet derivative along the pure-p basis vector and collapses the two-term sum by a Kronecker filter.
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}$ be site weights. For the assembled Hamiltonian $H_N(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N_j\, h(q_j,q_{j+1},p_j)$ on phase space of dimension $2$, the partial derivative of $H_N$ with respect to the momentum coordinate $p_k$ at any phase point $x$ equals $N_k\, h_p(q_k,q_{k+1},p_k)$.
background
This module is Wave C2 R5/R6 groundwork for the local-profile functional equation at $n=2$ (mirroring HamDyn). A local Hamiltonian profile is a map $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ evaluated on the triple $(q_j,q_{j+1},p_j)$. The assembled Hamiltonian is the weighted sum $H_N(x)=\sum_j N_j, h(q_j,q_{j+1},p_j)$ over the two cyclic sites.
Smoothness is packaged as a structure supplying three partial-profile maps $h_a,h_b,h_p$ together with a Fréchet-derivative witness: each cell map $y\mapsto h(y_1(j),y_1(j+1),y_2(j))$ has derivative $h_a,\mathrm{d}q_j+h_b,\mathrm{d}q_{j+1}+h_p,\mathrm{d}p_j$. The cell derivative operator and the summed derivative of $H_N$ are built from those witnesses.
The upstream lemma hasFDerivAt_LocalHamFromProfile asserts that $H_N$ is Fréchet differentiable with derivative equal to the weighted sum of cell derivatives. The private cell evaluation cellD_pdir records that feeding a pure-$p_k$ direction into a single cell derivative returns $h_p$ times the Kronecker $\delta_{jk}$.
proof idea
Unfold the momentum partial as the Fréchet derivative of $H_N$ applied to the pure-$p_k$ basis vector $(0,e_k)$. Replace that derivative by the summed cell derivative via hasFDerivAt_LocalHamFromProfile, then expand the sum of continuous-linear-map applications.
For each site index $j$, apply cellD_pdir: the $j$-th cell derivative on $(0,e_k)$ equals $h_p(q_j,q_{j+1},p_j)\cdot\mathbf{1}{j=k}$, and scaling by $N_j$ multiplies through. Congruence of the finite sum, followed by the standard identity that $\sum_j a_j\mathbf{1}{j=k}=a_k$, collapses everything to $N_k, h_p(q_k,q_{k+1},p_k)$.
why it matters
This identity is the $p$-half of the local-profile derivative calculus needed to reduce the dynamical Hamiltonian bracket at $n=2$. Downstream, local_profile_ham_ham_form uses both $p$- and $q$-partials to write
${H_N,H_M}=\sum_j(N_j M_{j+1}-M_j N_{j+1})\cdot C_j(h,S,x)$,
which is the R6 attack surface: the module doc states that this reduces Dyn ham_ham for local profiles to $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$, without yet proving rigidity.
It is also the concrete evaluation step inside vacuumKinetic_kinetic_regular_witness, which exhibits a nonzero $p$-partial of the vacuum kinetic density sum and thereby witnesses kinetic regularity for the normalized vacuum kinetic Hamiltonian. Within the SevenGaps gravity stack this is scaffolding for HKT local functional equations, not a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.