cellD_qdir
plain-language theorem explainer
Evaluating the local-cell Frechet derivative on a pure configuration basis vector isolates the two configuration partials ha and hb via Kronecker indicators on Z/2Z. Anyone assembling q-partials of a two-site local Hamiltonian profile cites this. The proof unfolds the continuous linear map and case-splits on the index equality in Z/2Z.
Claim. Let $h$ be a local Hamiltonian profile with smoothness data giving configuration partials $h_a$, $h_b$. For indices $j,k\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x$, the Frechet derivative of the $j$-th cell at $x$, applied to the pure $q$-direction basis vector $e_k$, equals $h_a(q_j,q_{j+1},p_j)\cdot\mathbf{1}_{j=k}+h_b(q_j,q_{j+1},p_j)\cdot\mathbf{1}_{j+1=k}$.
background
The module is Wave C2 R5/R6 groundwork for the local-profile functional equation at $n=2$ (mirroring HamDyn). It aims to reduce Dyn ham_ham for local profiles to the relation $\mathrm{momDensity}_j=h_b(j)\cdot h_p(j+1)$; rigidity is not yet proved.
A local Hamiltonian profile is a map $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, read as the cell contribution $h(q_j,q_{j+1},p_j)$. Smoothness data packages three profile maps $h_a$, $h_b$, $h_p$ together with a witness that each cell is Frechet-differentiable with derivative $h_a,\mathrm{coord}Q_j+h_b,\mathrm{coord}Q_{j+1}+h_p,\mathrm{coord}P_j$. The local-cell derivative is exactly that continuous linear map.
Phase space of dimension $2$ carries configuration and momentum coordinates indexed by $\mathbb{Z}/2\mathbb{Z}$. The coordinate functionals extract the $i$-th $q$ or $p$ component; pure $q$-directions are pairs $(\mathbf{e}_k,0)$.
proof idea
Unfold the local-cell derivative definition and apply the continuous-linear-map rules for addition and scalar multiplication, together with the simp lemmas for configuration/momentum coordinate evaluation and Pi.single. The momentum term vanishes on a pure $q$-direction. Case-split on $j=k$: when equal, prove $j+1\neq j$ in $\mathbb{Z}/2\mathbb{Z}$ by reducing to $1=0$, then simplify; when unequal, case-split on $j+1=k$ and simplify both residual branches.
why it matters
Direct input to the theorem computing the full $q$-partial of a Hamiltonian assembled from a local profile: that partial equals $N_k,h_a+N_{k-1},h_b$. The parent result is the R6 attack surface for the $n=2$ local-profile functional equation. The module reduces Dyn ham_ham for local profiles toward $\mathrm{momDensity}_j=h_b(j)\cdot h_p(j+1)$, but explicitly does not prove rigidity. This lemma is Gravity.SevenGaps scaffolding rather than a T0–T8 forcing-chain step; it supplies the configuration half of the cell derivative needed before any Poisson-bracket or functional-equation argument can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.