hasFDerivAt_localMomCell
plain-language theorem explainer
At each lattice cell j on the two-site phase space, a smooth local momentum profile f(d_j, π_j, π_{j+1}) is Fréchet differentiable, with derivative the packaged cell map built from the three partials. Anyone assembling smeared point-split momentum densities for the repaired HKT target cites this. The proof is a one-line wrapper that unpacks the smoothness structure field.
Claim. Let $f:\mathbb{R}^3\to\mathbb{R}$ be a local momentum profile and $S$ a smoothness package for $f$ (partials $f_d,f_p,f_r$ with cell Fréchet data). For every cell $j\in\mathbb{Z}/2\mathbb{Z}$ and every point $x$ of the two-site phase space, the map $y\mapsto f\bigl(q_{j+1}(y)-q_j(y),\,\pi_j(y),\,\pi_{j+1}(y)\bigr)$ is Fréchet differentiable at $x$, with derivative equal to the continuous linear cell map assembled from those partials at $x$.
background
This module repairs the Hojman–Kuchař–Teitelboim dynamic target after the unsplit momentum–Hamiltonian field proved uninhabitable for honest nearest-neighbor profiles against the frozen quadratic Hamiltonian at $n=2$. The load-bearing replacement uses smeared point-split momentum densities rather than an unsplit advection identity.
A local momentum profile is a function $f$ giving cell momenta $m_j=f(d_j,\pi_j,\pi_{j+1})$ with link $d_j=q_{j+1}-q_j$, hence translation-covariant by construction. The two-site phase space is pairs $(q,\pi)$ of maps $\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. The smoothness package stores three partial profiles and a cellwise Fréchet certificate; the packaged derivative is the continuous linear map $f_d,\mathrm{d}(q_{j+1}-q_j)+f_p,\mathrm{d}\pi_j+f_r,\mathrm{d}\pi_{j+1}$ evaluated at the cell data of $x$.
proof idea
One-line wrapper: apply the structure field hasFDerivCell of the smoothness package $S$ at the given cell $j$ and point $x$. No extra algebraic work; the derivative target is definitionally localMomCellD f S j x.
why it matters
Cellwise differentiability is the atomic step for smeared momentum functionals in the point-split HKT repair. The immediate parent is hasFDerivAt_MomFromProfile, which sums weighted cells via HasFDerivAt.fun_sum and constant multiplies by the smear weights, obtaining Fréchet differentiability of the full momentum-from-profile map.
That map feeds the strong point-split dynamic target (HKTPointSplitTargetDynStrong) after adjudication closed the unsplit Dyn route. The module records no rigidity theorem and flips no ledger flag; the open companion is the analogous unsplit obstruction against campaign HamDyn. Framework role is local to the gravity SevenGaps HKT sector, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.