cellD_pdir
plain-language theorem explainer
Evaluating the Fréchet derivative of one local Hamiltonian cell against a pure momentum basis vector returns the momentum partial coefficient times a Kronecker delta on the cell index. Anyone assembling p-partials of two-site local-profile Hamiltonians cites this. The argument is a short simplification of the continuous-linear-map definition plus a case split on index equality.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile with smooth data $(h_a,h_b,h_p)$, and let $D_j(x)$ be the Fréchet derivative of the $j$-th cell at phase-space point $x=(q,p)\in T^*\mathbb{R}^{\mathbb{Z}/2\mathbb{Z}}$. For indices $j,k\in\mathbb{Z}/2\mathbb{Z}$, $$D_j(x)\bigl(0,e_k\bigr)=h_p(q_j,q_{j+1},p_j)\cdot\mathbf{1}_{j=k},$$ where $e_k$ is the standard basis vector in the $k$-th momentum slot.
background
This module is Wave C2 groundwork for the local-profile functional equation at $n=2$ (mirroring HamDyn). The aim is to reduce the dynamical Hamiltonian identity for local profiles to the momentum-density relation $\mathrm{momDensity}_j=h_b(j),h_p(j+1)$; rigidity is not claimed.
A local Hamiltonian profile is a map $h:\mathbb{R}^3\to\mathbb{R}$ of neighbouring configurations and one momentum. Smoothness data packages three coefficient profiles $h_a,h_b,h_p$ together with the Fréchet derivative of each cell: the derivative of $y\mapsto h(q_j,q_{j+1},p_j)$ is the continuous linear map $h_a,\mathrm{coord}Q_j+h_b,\mathrm{coord}Q_{j+1}+h_p,\mathrm{coord}P_j$. That map is named localCellD in the file.
Phase space is the product of configuration and momentum fibres over $\mathbb{Z}/2\mathbb{Z}$. The coordinate maps $\mathrm{coord}Q_i$ and $\mathrm{coord}P_i$ extract the $i$-th configuration or momentum component; their evaluation lemmas are the only external ingredients.
proof idea
Term-mode proof by simplification. Unfold the cell derivative into the sum of three scaled continuous linear maps. Continuous-linear-map add and scalar-multiplication evaluation push the pure-momentum test vector $(0,e_k)$ through each summand. Configuration coordinates vanish on pure-momentum vectors; the momentum coordinate returns the Kronecker factor via Pi.single_apply. A by_cases on $j=k$ finishes both branches by simp.
why it matters
Feeds the parent theorem that computes the $p$-partial of a local-profile Hamiltonian: after summing cell derivatives, only the matching index survives, giving $\partial_{p_k}H=N_k,h_p(q_k,q_{k+1},p_k)$. That identity is the R6 attack surface for reducing the dynamical Hamiltonian constraint on two-site local profiles to a product of neighbouring coefficient profiles.
In the Recognition gravity stack this is pure calculus scaffolding inside the SevenGaps programme: it does not touch the forcing chain (T0–T8), the Recognition Composition Law, or the $\varphi$-ladder mass formula. It exists so later rigidity or uniqueness arguments for local Hamiltonians can quote an explicit $p$-derivative without reopening Fréchet bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.