pderivP_MomDyn_zero
plain-language theorem explainer
The p_0-partial of the smeared dynamic momentum MomDyn(w) equals (q_1 − q_0)(−w_1) on two-site phase space. Bracket identities for MomDyn against HamDyn, itself, and vacuum smears cite this evaluation. Proof rewrites the partial via the known Fréchet derivative MomDynD and simplifies the continuous-linear-map action on the p_0 basis vector.
Claim. For any weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,p)\in T^*\mathbb{R}^{2}$, the partial of the smeared momentum observable $\mathrm{MomDyn}(w):=\sum_j w_j\,\mathrm{momDynDensity}(x,j)$ in the momentum coordinate $p_0$ is $\partial_{p_0}\mathrm{MomDyn}(w)(x)=(q_1-q_0)(-w_1)$.
background
This module repairs the HKT dynamic target after the unsplit mom_ham field proved uninhabitable for nearest-neighbor local momentum against a frozen quadratic Hamiltonian at $n=2$. The load-bearing object is the strong point-split target; momentum is the smeared density already used in the Ham–Ham bracket, not a generator-symmetric sketch (vacuous on $\mathbb{Z}/2$ since $-1=1$).
Phase space is $T^*\mathbb{R}^{2}$ with configuration coordinates $q_i=x.1,i$ and momenta $p_i=x.2,i$. The smeared momentum is $\mathrm{MomDyn}(w)=\sum_{j\in\mathbb{Z}/2} w_j\cdot\mathrm{momDynDensity}(x,j)$. Its Fréchet derivative $\mathrm{MomDynD}$ is the product-rule map $(q_1-q_0)\cdot(w_0,\mathrm{coordP},1-w_1,\mathrm{coordP},0)+(w_0 p_1-w_1 p_0)\cdot(\mathrm{coordQ},1-\mathrm{coordQ},0)$.
The operator $\mathrm{pderivP},f,i$ is the directional derivative of $f$ along the pure $p_i$ basis vector. Upstream, hasFDerivAt_MomDyn identifies that derivative with evaluation of $\mathrm{MomDynD}$.
proof idea
One short rewrite-and-simp argument. Unfold $\mathrm{pderivP}$ and replace the Fréchet derivative by $\mathrm{MomDynD}$ via hasFDerivAt_MomDyn. Then simp with continuous-linear-map add_apply / smul_apply and the coordinate lemmas coordQ_apply, coordP_apply.
Only the first summand of $\mathrm{MomDynD}$ survives on a pure $p_0$ direction: $\mathrm{coordP},0$ contributes $1$, $\mathrm{coordP},1$ and both $\mathrm{coordQ}$ vanish, leaving $(q_1-q_0)\cdot(-w_1)$.
why it matters
Supplies the $p$-leg needed to expand Poisson brackets of the point-split momentum sector. Downstream it is used by bracket_MomDyn_MomDyn (Wronskian density, momentum sector non-abelian), bracket_MomDyn_HamDyn (source/target advection form of mom–ham), and bracket_MomDyn_VacSmear in the vacuum-sector kill module.
In the SevenGaps HKT campaign this is API glue for the Wave C2 R5 point-split repair: honest $n=2$ smeared momentum against dynamic/vacuum Hamiltonians, after unsplit advection was ruled out. No rigidity theorem and no ledger flag are claimed here; the result only closes derivative bookkeeping so the bracket identities can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.