localMomCellD_pdir
plain-language theorem explainer
Evaluating the Fréchet cell derivative of a local nearest-neighbor momentum profile on a pure momentum basis vector retains only the two momentum partials of the profile, each gated by a Kronecker indicator on the cell endpoints. Anyone assembling p-partials of smeared point-split momentum densities on the two-site phase space cites this. The proof unfolds the continuous-linear combination and case-splits the two endpoint equalities.
Claim. Let $f$ be a local momentum profile $m_j=f(q_{j+1}-q_j,\pi_j,\pi_{j+1})$ with smooth cell data $(f_d,f_p,f_r)$. For $j,k\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x$, the Fréchet cell derivative of $f$ at $x$ applied to the pure momentum basis vector $e_k^p=(0,\mathbf{1}_k)$ equals $f_p(\Delta q_j,\pi_j,\pi_{j+1})\,\mathbf{1}_{j=k}+f_r(\Delta q_j,\pi_j,\pi_{j+1})\,\mathbf{1}_{j+1=k}$.
background
This module is the Wave C2 R5 repair of the Hojman–Kuchař–Teitelboim dynamic target: the unsplit momentum–Hamiltonian field is uninhabitable for honest nearest-neighbor local momentum profiles against a frozen quadratic Hamiltonian at $n=2$. The repaired API uses smeared point-split momentum densities with source/target advection.
A local momentum profile is a map $f:\mathbb{R}^3\to\mathbb{R}$ giving $m_j=f(d_j,\pi_j,\pi_{j+1})$ with $d_j=q_{j+1}-q_j$, translation-covariant by construction. The smoothness package supplies Fréchet cell data $f_d,f_p,f_r$ and a HasFDerivAt witness that each cell differentiates as a continuous-linear combination of configuration and momentum coordinate functionals.
The cell derivative is exactly that map: $f_d\cdot(\mathrm{coord}_Q(j+1)-\mathrm{coord}_Q j)+f_p\cdot\mathrm{coord}_P j+f_r\cdot\mathrm{coord}_P(j+1)$. Phase space is the product of configuration and momentum sections over $\mathbb{Z}/2\mathbb{Z}$; coordinate evaluation lemmas identify $\mathrm{coord}_P i,x=x_2(i)$.
proof idea
Short tactic proof by unfolding and case analysis. Unfold the cell-derivative definition and simplify with continuous-linear-map add/smul rules, the coordinate evaluation lemmas for $q$ and $p$, and Pi.single_apply. The pure-momentum test vector annihilates every configuration coordinate, so the $f_d$ term drops. The two remaining terms reduce to $f_p$ or $f_r$ times a unit or zero according as $j=k$ or $j+1=k$. Nested case splits on those two equalities close all four combinatorial branches by simplification.
why it matters
Direct input to the theorem that computes the full $p$-partial of the smeared momentum density built from a local profile: that identity rewrites the partial as a two-cell weighted sum of $f_p$ and $f_r$. The partial is load-bearing for the strong point-split HKT dynamic target, the repaired sibling of the unsplit Dyn target after the Wave C2 R5 adjudication.
Within the SevenGaps gravity campaign this supports honest local structure for hypersurface-deformation brackets on the two-site phase space. The module records that the momentum sector is non-abelian (Wronskian density in the momentum–momentum bracket) and proves no rigidity theorem; no ledger flag is flipped. The result is internal calculus infrastructure, not a forcing-chain step (T0–T8) or an instance of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.