MomDyn_closed
plain-language theorem explainer
On two-site phase space the smeared point-split momentum functional collapses to the bilinear closed form (q₁ − q₀)(w₀ p₁ − w₁ p₀). Anyone differentiating MomDyn or matching product-rule frechet forms cites this identity. The proof unfolds the density sum on ZMod 2 and finishes by ring.
Claim. For any smear weights $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and any point $x=(q,p)$ in two-site phase space, the smeared momentum $\mathrm{MomDyn}(w,x):=\sum_j w(j)\,p_{j+1}(q_{j+1}-q_j)$ equals $(q_1-q_0)(w_0 p_1-w_1 p_0)$.
background
This module repairs the HKT dynamic target after the unsplit mom_ham field proved uninhabitable for smooth nearest-neighbor momentum profiles against a frozen quadratic Hamiltonian at $n=2$. The load-bearing replacement uses a smeared point-split momentum density already present in the HamDyn/Ham brackets, with source/target advection densities kept separate.
momDynDensity at site $j$ is $p_{j+1}(q_{j+1}-q_j)$. MomDyn smears that density against weights $w$ on $\mathbb{Z}/2\mathbb{Z}$. On two sites one has $1+1=0$ in $\mathbb{Z}/2\mathbb{Z}$, so the two-term sum is elementary; the private lemmas sum_zmod2 and the $1+1=0$ facts discharge the discrete bookkeeping.
Phase space is the product of configuration and momentum fields on two lattice sites. No rigidity claim is made here; the identity is pure algebra on that finite sum.
proof idea
Term-mode proof by unfolding. Expand MomDyn into the weighted sum of momDynDensity, then expand each density. Apply sum_zmod2 to replace the $\mathbb{Z}/2\mathbb{Z}$ sum by the two explicit terms at $0$ and $1$, and use zmod2_zero_add_one / zmod2_one_add_one so indices $j+1$ evaluate correctly. The resulting four-factor polynomial identity is discharged by ring.
why it matters
Feeds hasFDerivAt_MomDyn, which needs the closed product form so the frechet derivative matches the product-rule shape $f,g'+g,f'$ from HasFDerivAt.mul / .sub. That derivative is part of the repaired point-split HKT dynamic target (HKTPointSplitTargetDynStrong lineage) after the unsplit Dyn mom_ham was ruled out for honest nearest-neighbor profiles.
In the SevenGaps gravity campaign this is bookkeeping infrastructure, not a physics law: it makes the momentum sector of the point-split bracket calculus differentiable in Lean. It does not flip ledger flags or close the open unsplit-vs-HamDyn witness prop. Framework landmarks T0–T8 are upstream of this discrete HKT repair and are not invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.