MomDyn
plain-language theorem explainer
Smeared point-split momentum on the two-site lattice phase space: a weight profile times nearest-neighbor momentum density, summed over Z/2Z. Gravity and HKT-target authors cite it as the honest momentum sector after the unsplit mom_ham obstruction. The body is a one-line weighted sum of momDynDensity; no proof content.
Claim. For a weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,\pi)$ on the $2$-site periodic lattice, the smeared point-split momentum is $\mathrm{MomDyn}(w,x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\,\pi_{j+1}(q_{j+1}-q_j)$.
background
Phase space on $n$ sites is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$. The local density momDynDensity at site $j$ is the nearest-neighbor product $\pi_{j+1}(q_{j+1}-q_j)$: momentum one step ahead times the configuration jump across the bond.
This module repairs the widened Hojman–Kuchař–Teitelboim dynamic target. The unsplit mom_ham field is uninhabitable for smooth nearest-neighbor momentum against a frozen quadratic Hamiltonian (singular when $p_0+p_1=0$). The repair replaces that field by smeared point-split momentum densities already used in the Hamiltonian–Hamiltonian bracket, with source/target advection densities.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the generator-symmetric deformation vanishes and cannot carry the split. The momentum sector is deliberately non-abelian: the mom–mom bracket carries a Wronskian density rather than zero.
proof idea
Definitional one-liner: expand as the finite sum over $j:\mathbb{Z}/2\mathbb{Z}$ of $w(j)$ times momDynDensity x j. No lemmas, no tactics; pure weighted smear of the local bond density.
why it matters
Load-bearing API atom for the point-split HKT program at $n=2$. Downstream brackets bracket_MomDyn_HamDyn and bracket_MomDyn_MomDyn compute the Poisson structure of this smear against Hamiltonian and momentum sectors; differentiable_MomDyn supplies smoothness. Strong target inhabitants (hamDynPointSplitTargetStrong, vacuumKineticStrongTarget) witness non-degeneracy via hamDyn_mom_load_bearing_witness: the bracket of MomDyn delta0 against MomDyn delta1 is nonzero at a fixed phase point. Kinetic-normalized rigidity theorems (mom_ham_split_vacuumKinetic and the vacuum kinetic weak/strong targets) plug this functional in as the momentum density of the repaired Dyn schema. No rigidity is proved in this module; the definition only makes the honest split target inhabitable after the unsplit obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.