localMomCellD_qdir
plain-language theorem explainer
On the two-site phase space, the Fréchet cell derivative of a local momentum profile, evaluated on a pure configuration basis vector at site k, collapses to the d-partial of the profile times an indicator difference (1_{j+1=k} − 1_{j=k}). Anyone computing configuration partials of smeared point-split momentum densities cites this. The proof is a short case split on the two ZMod-2 equalities after unfolding the cell map and coordinate projections.
Claim. Let $f:\mathbb{R}^3\to\mathbb{R}$ be a local momentum profile $m_j=f(q_{j+1}-q_j,\pi_j,\pi_{j+1})$ with smoothness data $S$ (partials $f_d,f_p,f_r$). For $j,k\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x$, the cell derivative $D_j f(x)$ applied to the pure $q$-basis vector $e_k^q=(\delta_k,0)$ equals $f_d(q_{j+1}-q_j,\pi_j,\pi_{j+1})\cdot\bigl(\mathbf{1}_{j+1=k}-\mathbf{1}_{j=k}\bigr)$.
background
This module repairs the Hojman–Kuchař–Teitelboim dynamic target after the unsplit momentum–Hamiltonian sector proved uninhabitable for nearest-neighbor local profiles against the frozen quadratic Hamiltonian at $n=2$. The load-bearing object is the strong point-split target; momentum is carried by smeared point-split densities rather than an unsplit advection field.
A local momentum profile is a map $f$ with cell values $m_j=f(d_j,\pi_j,\pi_{j+1})$ and link $d_j=q_{j+1}-q_j$, translation-covariant by construction. The smoothness package supplies Fréchet cell data: partials $f_d$, $f_p$, $f_r$ and a HasFDerivAt witness. The cell derivative is the continuous linear map
$D_j f(x)=f_d,(\mathrm{coord}Q_{j+1}-\mathrm{coord}Q_j)+f_p,\mathrm{coord}P_j+f_r,\mathrm{coord}P_{j+1}$.
Configuration and momentum coordinates on PhaseSpace 2 are the standard projections; evaluating on $(\mathrm{Pi.single},k,1,,0)$ isolates the pure $q_k$ direction used by partials pderivQ.
proof idea
Unfold localMomCellD and apply linearity of continuous linear maps (add_apply, smul_apply). The $p$-legs vanish on a pure $q$-vector by coordP_apply; the $q$-legs reduce by coordQ_apply and Pi.single_apply to the two indicators $1_{j+1=k}$ and $1_{j=k}$. Two nested by_cases on $j=k$ and $j+1=k$, followed by simp, discharge the four Boolean combinations (on $\mathbb{Z}/2\mathbb{Z}$ the cases $j=k$ and $j+1=k$ are mutually exclusive).
why it matters
Feeds pderivQ_MomFromProfile, which assembles the configuration partial of the smeared momentum density MomFromProfile as a weighted difference of neighboring $f_d$ cells. That identity is the $q$-sector input to Poisson brackets in the point-split HKT repair (bracket_HamDyn_HamDyn / momentum–Hamiltonian coupling via hamAdvFrom / hamAdvTo).
In the Seven Gaps gravity campaign this is bookkeeping for Wave C2 R5: after adjudication that unsplit mom_ham is singular on $p_0+p_1=0$, the honest $n=2$ API uses smeared point-split momentum. No rigidity theorem is claimed here; the lemma only evaluates one directional derivative needed to inhabit the strong point-split target. Framework-wise it sits in the classical hypersurface-deformation algebra that HKT use to recover geometrodynamics, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.