DgenSym_eq_zero_two
plain-language theorem explainer
On the two-site periodic lattice the symmetric-difference momentum generator vanishes for every shift and every phase-space point. Gravity workers on the HKT point-split repair at n=2 cite this to show a DgenSym-shaped momentum-Hamiltonian split is empty. The proof reduces the lattice sum after using that every class in Z/2Z equals its additive inverse.
Claim. For every $a \in \mathbb{Z}/2\mathbb{Z}$ and every phase-space point $x=(q,\pi)$ on the two-site lattice, the symmetric-difference momentum generator $D^{\mathrm{sym}}_a[q,\pi]=\tfrac12\sum_i \pi_i(q_{i+a}-q_{i-a})$ equals $0$.
background
Phase space on an $n$-site periodic lattice is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. The symmetric-difference momentum generator is the model functional $D^{\mathrm{sym}}a[q,\pi]=\tfrac12\sum_i \pi_i(q{i+a}-q_{i-a})$. Upstream, that generator is the antisymmetric discrete difference that restores closure of the momentum-Hamiltonian bracket on larger lattices (via discrete integration by parts with no boundary).
This module is the Wave C2 R5 repair of the point-split Hojman-Kuchař-Teitelboim dynamic target. The unsplit Dyn target keeps an unsplit momentum-Hamiltonian field that is uninhabitable for honest nearest-neighbor local momentum profiles against the frozen quadratic Hamiltonian at $n=2$. The repaired sibling therefore works with smeared point-split momentum densities.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the two shifts $i+a$ and $i-a$ coincide for every $a$. The module doc records the consequence: $D^{\mathrm{sym}}_a\equiv 0$ as a functional and the Poisson bracket ${D^{\mathrm{sym}}_a,\cdot}$ is vacuous.
proof idea
Unfold the definition of the symmetric-difference generator to a finite sum over $\mathbb{Z}/2\mathbb{Z}$. Reduce to showing each summand vanishes via Finset.sum_eq_zero.
For fixed site $i$ and shift $a$, prove $i+a=i-a$ in $\mathbb{Z}/2\mathbb{Z}$. The key algebraic fact is $a+a=0$ for every $a$ (checked by fin_cases and decide). Rewrite $i+a$ as $i-a+(a+a)$, cancel the zero, and conclude equality. Substitute into the difference $q_{i+a}-q_{i-a}$ and simplify the summand to zero.
why it matters
Documentary role: because the generator is identically zero at two sites, any momentum-Hamiltonian split written in DgenSym shape is definitionally empty at the HamDyn size. The module therefore abandons that sketch and uses smeared point-split advection densities instead.
Downstream, the weak rigidity statement HKTRigidityStatementPointSplitDynN2 quantifies over the weak point-split Dyn schema; this vanishing fact is part of the n=2 API adaptation that schema inherits. Binding rigidity is deferred to the strong class; the module explicitly proves no rigidity theorem and flips no ledger flag.
In the broader SevenGaps gravity program this is a local lattice identity, not a forcing-chain step (T0-T8). It clears a false path so the repaired point-split target can be stated honestly against the frozen quadratic Hamiltonian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.