localMomCellD
plain-language theorem explainer
Packages the Fréchet derivative of one nearest-neighbor momentum cell on the two-site lattice as a continuous linear map on phase space. Anyone building smeared point-split momentum densities for the repaired HKT dynamic target cites it. The body is the chain-rule expansion in the configuration difference and the two adjacent momenta, using the three partials from the smoothness package.
Claim. Given a local momentum profile $f:\mathbb{R}^3\to\mathbb{R}$ (so $m_j=f(q_{j+1}-q_j,\pi_j,\pi_{j+1})$) and smoothness data $S$ supplying partials $\partial_d f$, $\partial_{\pi_j}f$, $\partial_{\pi_{j+1}}f$, for each site $j\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x$, define the continuous linear map $Dm_j(x):T_x\mathrm{PhaseSpace}_2\to\mathbb{R}$ by $$Dm_j(x)=(\partial_d f)\,(dq_{j+1}-dq_j)+(\partial_{\pi_j}f)\,d\pi_j+(\partial_{\pi_{j+1}}f)\,d\pi_{j+1},$$ with partials evaluated at $(q_{j+1}-q_j,\pi_j,\pi_{j+1})$.
background
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target. The unsplit mom_ham field is uninhabitable for honest nearest-neighbor local momentum against the frozen quadratic Hamiltonian at $n=2$: unsplit advection forces a singular identity on $p_0+p_1=0$. The repaired sibling uses smeared point-split momentum densities instead.
Phase space is the product $(q,\pi)$ of configuration and conjugate momentum on the periodic lattice $\mathbb{Z}/2\mathbb{Z}$. Coordinate functionals $dq_i$ and $d\pi_i$ are the continuous linear projections. A local momentum profile is a map $f$ 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 three partial profiles $(\partial_d f,\partial_{\pi_j}f,\partial_{\pi_{j+1}}f)$ together with a cellwise HasFDerivAt witness that this linear combination is indeed the Fréchet derivative of the cell map.
proof idea
Pure definitional term, not a proved lemma. It assembles three scaled continuous linear maps: the configuration-difference functional $dq_{j+1}-dq_j$ scaled by the $d$-partial, plus $d\pi_j$ scaled by the first momentum partial, plus $d\pi_{j+1}$ scaled by the second momentum partial, all partials evaluated at the cell arguments $(q_{j+1}-q_j,\pi_j,\pi_{j+1})$. The matching HasFDerivAt fact is recorded separately as a one-line wrapper of the smoothness package's cell witness.
why it matters
Load-bearing cell derivative for the point-split momentum sector of the repaired HKT dynamic target. Downstream, hasFDerivAt_localMomCell re-exports the Fréchet fact; MomFromProfileD smears the cells with a weight $w$ as $\sum_j w_j,Dm_j$; and the partial-derivative theorems for the smeared momentum density expand $p$- and $q$-directional derivatives by evaluating this map on basis increments. Those expansions feed the non-abelian mom_mom bracket (Wronskian density, not zero) that replaces the vacuous $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch at $n=2$ (where $-1=1$). No rigidity theorem is claimed here; the unsplit Dyn target stays as the falsification-adjacent record, and the campaign-HamDyn analogue remains an open Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.