bracket_MomDyn_HamDyn
plain-language theorem explainer
On the two-site phase space, the Poisson bracket of the smeared dynamic momentum against the smeared dynamic Hamiltonian equals the weighted sum of point-split advection fluxes: each site contributes w_j times (N_{j+1} times the target density minus N_j times the source density). Anyone assembling the honest n=2 HKT point-split dynamic target cites this identity. The proof expands both sides over ZMod 2, substitutes the known partials, freezes the modular shifts, and closes by ring.
Claim. Let $w,N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ be smearing weights and lapse values, and let $x$ be a point of the two-site phase space. The canonical Poisson bracket of the smeared dynamic momentum functional $M_w$ with the smeared dynamic Hamiltonian $H_N$ equals $\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w_j\bigl(N_{j+1}\,A^{\mathrm{to}}_j(x)-N_j\,A^{\mathrm{from}}_j(x)\bigr)$, where $A^{\mathrm{to}}_j$ and $A^{\mathrm{from}}_j$ are the dynamic Hamiltonian advection densities at site $j$.
background
This module repairs the unsplit dynamic HKT target. The unsplit mom-ham field is uninhabitable for honest nearest-neighbor local momentum profiles against a frozen quadratic Hamiltonian at $n=2$: unsplit advection forces a singular identity on the zero-total-momentum locus. The repaired sibling uses a smeared point-split momentum density together with source and target advection densities, matching the pattern already used for the Hamiltonian-Hamiltonian bracket.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the antisymmetric generator that appears in the adjudicated sketch is definitionally zero; the structure therefore works directly with the smeared densities. The dynamic momentum $M_w$ is the $w$-weighted sum of the local dynamic momentum densities. The dynamic Hamiltonian $H_N$ is the analogous $N$-smearing of the quadratic dynamic Hamiltonian density. The ambient Poisson bracket is the standard sum over sites of $\partial_q F,\partial_p G-\partial_p F,\partial_q G$.
The local theoretical setting is Wave C2 R5: no rigidity theorem is claimed here, and no ledger flag is flipped. The load-bearing class is the strong point-split target; the weak schema remains only as a demoted record.
proof idea
Tactic proof by direct expansion. First rewrite the left-hand bracket via the two-term $\mathbb{Z}/2\mathbb{Z}$ sum of canonical pairs, and expand the right-hand weighted sum the same way (using the elementary facts $0+1=1$ and $1+1=0$).
Next substitute the four partial-derivative evaluations of $H_N$ at sites $0$ and $1$, together with the four partials of $M_w$ (vanishing or weight-times-density as appropriate). Freeze all modular shifts with the four $\mathbb{Z}/2\mathbb{Z}$ add/sub lemmas, then unfold the source and target advection densities.
The resulting equality is a polynomial identity in the eight phase-space scalars; ring discharges it. No external analytic lemma is required beyond the already-proved partials of the dynamic momentum and Hamiltonian smearings.
why it matters
This identity is the mom-ham half of the structure equations needed to inhabit the repaired point-split dynamic HKT target at $n=2$. Downstream, hamDynPointSplitTarget packages the dynamic densities and advection maps into an honest inhabitant of that target; the present bracket supplies the mom-ham field of that package.
It is also reused by the vacuum-sector kill lemma that computes the analogous bracket of dynamic momentum against the vacuum Hamiltonian shift, and it sits under the (demoted) weak rigidity statement over the point-split schema. Binding rigidity is deferred to the strong class; the module doc is explicit that no rigidity theorem is proved here.
In the broader Seven Gaps gravity program this is bookkeeping for the Hojman-Kuchař-Teitelboim constraint algebra on a discrete two-site circle, not a derivation of $D=3$ or of the eight-tick octave. It closes the honest nearest-neighbor gap left by the unsplit dynamic target without claiming uniqueness of the quadratic kinetic sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.