pderivQ_MomFromProfile
plain-language theorem explainer
Explicit formula for the configuration-space partial of the smeared nearest-neighbor momentum functional on the two-site phase space. HKT/gravity workers cite it when evaluating Poisson brackets of MomFromProfile against the frozen quadratic Hamiltonian. The proof expands the Fréchet derivative cellwise and collapses the Z/2Z sum by indicator identities.
Claim. Let $f$ be a local momentum profile $m_j=f(q_{j+1}-q_j,\pi_j,\pi_{j+1})$ with smoothness data $S$ (partials $S_{f_d}$, $S_{f_p}$, $S_{f_r}$), let $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ be a smear weight, and let $x$ be a point of the two-site phase space. Then the partial derivative of $\mathrm{Mom}_f[w]$ in the $q_k$ direction is $w(k-1)\,S_{f_d}(q_k-q_{k-1},\pi_{k-1},\pi_k)-w(k)\,S_{f_d}(q_{k+1}-q_k,\pi_k,\pi_{k+1})$.
background
This module repairs the unsplit Dyn-style HKT target. The widened dynamic target keeps an unsplit momentum-Hamiltonian field that is uninhabitable for honest nearest-neighbor local momentum profiles against the frozen quadratic Hamiltonian: at $n=2$, unsplit advection forces a singular identity on $p_0+p_1=0$. The repaired sibling works with smeared point-split momentum densities already used in the HamDyn brackets.
A local momentum profile is a map $f:\mathbb{R}^3\to\mathbb{R}$ giving cell momenta $m_j=f(d_j,\pi_j,\pi_{j+1})$ with link $d_j=q_{j+1}-q_j$, translation-covariant by construction. Smoothness packages supply Fréchet cell data: partials $S.fd$, $S.fp$, $S.fr$ and a HasFDerivAt witness per cell. The smeared momentum is $\mathrm{Mom}_fw=\sum_j w_j,m_j(x)$ on PhaseSpace 2 (configuration and momentum sections over $\mathbb{Z}/2\mathbb{Z}$).
The quantity computed here is the directional derivative of that functional in a pure $q_k$ direction, the building block for Poisson brackets against the frozen quadratic Hamiltonian density.
proof idea
Unfold the configuration partial as the Fréchet derivative of MomFromProfile applied to the pure $q_k$ unit vector, using the already-proved HasFDerivAt witness and the explicit derivative map MomFromProfileD. The derivative is a sum over cells of weighted localMomCellD maps.
For each cell $j$, evaluate the cell derivative on $(\mathrm{Pi.single},k,1,,0)$. The $q$-direction formula for localMomCellD contributes only through the two endpoints of the link, producing the factor $(\mathbf{1}{j+1=k}-\mathbf{1}{j=k})$ times $w_j S.fd$ on that cell. Sum the resulting two-term expression, distribute, and apply the finite-sum indicator lemmas that pick out the unique $j$ with $j=k$ and the unique $j$ with $j+1=k$. The latter rewrites as $j=k-1$ after the ring identity $k-1+1=k$ on $\mathbb{Z}/2\mathbb{Z}$.
why it matters
Feeds the no-go evaluation bracket_MomFromProfile_delta0_unsplitNoGo, which at the witness weight $w=\delta_0$ and the singular phase-space point computes ${\mathrm{Mom},\mathrm{Ham},N}=(N_0+N_1)(-\partial_d f+\partial_p f-\partial_r f)$. That identity is the concrete obstruction showing unsplit Dyn-style advection cannot be realized by smooth nearest-neighbor profiles against the frozen quadratic Hamiltonian.
In the SevenGaps gravity program this is part of the Wave C2 R5 point-split HKT repair: the unsplit Dyn target stays as a falsification-adjacent record, while the load-bearing class is the strong point-split target with source/target advection densities. No rigidity theorem is claimed here, and no ledger flag is flipped. The calculation is local to $n=2$ (where $-1=1$ on $\mathbb{Z}/2\mathbb{Z}$ collapses the symmetric generator), matching the honest narrow scope of the adjudication note.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.