MomFromProfileD
plain-language theorem explainer
Fréchet derivative of the smeared local-momentum functional on the two-site lattice phase space: a weighted sum of the cellwise derivatives of a translation-covariant profile m_j = f(d_j, π_j, π_{j+1}). Anyone computing momentum-sector brackets or p/q partials in the point-split HKT target cites it. The body is a two-term sum of scaled continuous-linear cell maps.
Claim. Let $f:\mathbb{R}^3\to\mathbb{R}$ be a local momentum profile with smoothness data $S$ (partials $f_d,f_p,f_r$ and cell Fréchet certificates), let $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ be smear weights, and let $x$ be a point of the two-site phase space $(q,\pi)$. Define the continuous linear map $D_x M_w:\mathrm{PhaseSpace}_2\to_L\mathbb{R}$ by $D_x M_w=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\,D_x m_j$, where $D_x m_j$ is the Fréchet derivative of the $j$-th local momentum cell at $x$.
background
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target: the unsplit mom_ham field is uninhabitable for smooth nearest-neighbour momentum profiles against a frozen quadratic Hamiltonian at $n=2$ (singularity on $p_0+p_1=0$). The repaired API uses a smeared point-split momentum density on $\mathbb{Z}/2\mathbb{Z}$.
Phase space is the product $(q,\pi)$ of configuration and conjugate momentum on the periodic two-site lattice. A local momentum profile is a map $f$ with cell values $m_j=f(q_{j+1}-q_j,\pi_j,\pi_{j+1})$, translation-covariant by construction. The smoothness package supplies the three partial profiles and a cellwise HasFDerivAt certificate.
The cell derivative localMomCellD assembles those partials against the coordinate functionals $\mathrm{coord}Q(j+1)-\mathrm{coord}Q(j)$, $\mathrm{coord}P(j)$, and $\mathrm{coord}P(j+1)$. The present definition smears those cell maps by weights $w$.
proof idea
Pure definition: no proof obligations. The value is the finite sum over $j:\mathbb{Z}/2\mathbb{Z}$ of the scalar multiple $(w,j)\bullet(\mathrm{localMomCellD},f,S,j,x)$, i.e. the $w$-weighted superposition of the two continuous-linear cell derivatives already packaged by the smoothness structure.
why it matters
Load-bearing derivative object for the point-split HKT momentum sector after the Wave C2 R5 adjudication. Downstream, hasFDerivAt_MomFromProfile certifies that this map is the Fréchet derivative of the smeared functional MomFromProfile; the partial-extraction theorems pderivP_MomFromProfile and pderivQ_MomFromProfile then read off $\partial_{\pi_k}$ and $\partial_{q_k}$ by evaluating the fderiv against coordinate directions.
Those partials feed bracket identities (mom_mom carries a Wronskian density, not zero) inside the strong point-split target class. No rigidity theorem is claimed here, and no ledger flag is flipped; the definition only makes the derivative data available so the repaired dynamic target can be inhabited honestly at $n=2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.