MomFromProfile
plain-language theorem explainer
Smeared momentum density on the two-site lattice: weight a local nearest-neighbor momentum profile by a test function on Z/2Z and sum. Gravity and HKT-target authors cite it as the honest replacement for unsplit mom_ham when checking Poisson brackets against frozen quadratic or HamDyn Hamiltonians. The body is a two-term weighted sum of the pointwise profile evaluation.
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})$), a weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, and a phase-space point $x=(q,\pi)$ on the $n=2$ periodic lattice, define the smeared momentum $$M_f[w](x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\,f\bigl(q_{j+1}-q_j,\pi_j,\pi_{j+1}\bigr).$$
background
This module repairs the Hojman–Kuchař–Teitelboim dynamic target after the unsplit mom_ham field proved 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 API uses a smeared point-split momentum density instead.
Phase space is the product of configuration and conjugate momentum on the periodic lattice: $x=(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. A local momentum profile is a function $f$ of the bond length $d_j=q_{j+1}-q_j$ and the two endpoint momenta, hence translation-covariant by construction. The pointwise evaluation at site $j$ is $f(d_j,\pi_j,\pi_{j+1})$; the present definition only smears that cell density by a weight $w$.
At $n=2$ one has $-1=1$ in $\mathbb{Z}/2\mathbb{Z}$, so the older $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch is definitionally empty. The load-bearing class is the strong point-split target; no rigidity theorem is claimed in this file.
proof idea
Pure definition: expand as the finite sum over $j\in\mathbb{Z}/2\mathbb{Z}$ of $w(j)$ times the pointwise profile evaluation at site $j$. No lemmas, no tactics. Downstream Fréchet and partial-derivative lemmas unfold this sum and apply the cellwise derivative of the local profile.
why it matters
This is the momentum sector used throughout the point-split HKT repair. Downstream it feeds the Fréchet derivative of the smeared momentum, the $p$- and $q$-partials, the unsplit advection identity against the frozen quadratic Hamiltonian, and the open HamDyn analogue. The bracket identity at the no-go witness with $w=\delta_0$ reduces ${M,H_N}$ to a multiple of $-\partial_d f+\partial_p f-\partial_r f$, which is the concrete obstruction to smooth nearest-neighbor unsplit advection.
In the Recognition gravity stack this sits inside the SevenGaps HKT campaign: the unsplit Dyn target remains as a falsification-adjacent record, while the strong point-split target is the repaired sibling. Finding already recorded in the module: the momentum sector is not abelian (the mom–mom bracket carries a Wronskian density). No ledger flag is flipped here; the open Prop is the HamDyn-level unsplit no-go.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.