bracket_MomDyn_MomDyn
plain-language theorem explainer
On the two-site phase space, the Poisson bracket of two smeared dynamic momenta Mom(v) and Mom(w) equals a discrete Wronskian times a local density: sum_j (v_j w_{j+1} - w_j v_{j+1}) · momDynBracketDensity(x,j). Anyone building or auditing the point-split HKT momentum sector cites this identity. The proof expands the canonical bracket on ZMod 2, substitutes the explicit partials of MomDyn, and reduces by ring.
Claim. For weight functions $v,w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x$, the Poisson bracket of the smeared dynamic momenta satisfies $\{M_v,M_w\}(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}}(v_j w_{j+1}-w_j v_{j+1})\,\rho_{\mathrm{br}}(x,j)$, where $M_u=\sum_j u_j\,m(x,j)$ and $\rho_{\mathrm{br}}(x,j)=\frac12(q_{j+1}-q_j)(p_j+p_{j+1})$ is the true $\{M,M\}$ Wronskian density.
background
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target at $n=2$. The unsplit mom_ham field is uninhabitable for honest nearest-neighbor local momentum against a frozen quadratic Hamiltonian (singular when $p_0+p_1=0$). The repaired API uses smeared point-split momentum densities already present in the Ham–Ham bracket identities, with source/target advection densities.
MomDyn v is the linear smear $\sum_j v_j,m(x,j)$ of the dynamic momentum density on PhaseSpace 2. The companion density momDynBracketDensity is documented as the true ${M,M}$ Wronskian density at $n=2$: $\frac12(q_{j+1}-q_j)(p_j+p_{j+1})$. On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the symmetric generator is definitionally empty; the momentum sector is therefore not forced abelian.
Upstream arithmetic is elementary: sum_zmod2 expands finite sums over ${0,1}$, and $1+1=0$ in $\mathbb{Z}/2\mathbb{Z}$ rewrites the cyclic neighbor indices.
proof idea
Expand the left-hand side by unfolding the canonical Poisson bracket and applying sum_zmod2, so the bracket is the sum of the two site contributions $( \partial_q M_v,\partial_p M_w - \partial_p M_v,\partial_q M_w)$ at $j=0$ and $j=1$.
Expand the right-hand side the same way with sum_zmod2, then rewrite neighbors via $0+1=1$ and $1+1=0$. Substitute the eight explicit partials of MomDyn at sites $0$ and $1$ (the pderivQ_MomDyn_* and pderivP_MomDyn_* lemmas). Unfold momDynBracketDensity and finish by ring.
why it matters
Module finding: the momentum sector is not abelian; mom_mom carries a Wronskian density, not zero. This identity is the algebraic content of that claim and is the load-bearing computation behind hamDyn_mom_load_bearing_witness, which exhibits a concrete phase-space point where ${M_{\delta_0},M_{\delta_1}}\neq 0$.
It feeds the honest HamDyn inhabitant hamDynPointSplitTarget of the repaired point-split Dyn target, and is reused by weak vacuum/kinetic targets (vacuumKineticWeakTarget, vacuumShiftWeakTarget) that share the same momentum density. The weak rigidity statement HKTRigidityStatementPointSplitDynN2 quantifies over this schema; binding rigidity is the Strong sibling. No ledger flag is flipped here, and no full HKT rigidity theorem is proved in this module.
In the SevenGaps gravity campaign this is pure classical field-bracket bookkeeping on a two-tick lattice, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.