bracket_HamDynN_HamDynN
plain-language theorem explainer
The Poisson bracket of two general-n dynamic Hamiltonians with lapses N and M equals a cyclic sum of (N_j M_{j+1} - M_j N_{j+1}) times the left-split structure factor (1+q_j^2) and the momentum-weighted bond stretch. Gravity and continuum-binding proofs cite it as the exact dynamic structure identity beyond the two-site case. The proof unfolds the bracket, cancels ∂g/∂q terms by ring algebra, then reindexes the periodic lattice sum by one site.
Claim. For lapses $N,M:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,p)$, the Poisson bracket of the dynamic Hamiltonians satisfies $\{H_N^{\mathrm{dyn}},H_M^{\mathrm{dyn}}\}(x)=\sum_j(N_j M_{j+1}-M_j N_{j+1})\,(1+q_j^2)\,p_{j+1}(q_{j+1}-q_j)$.
background
The module repairs Wave C2 R4 Step 2: it lifts the two-site dynamic structure bracket to arbitrary lattice size $n$ with $[\mathrm{NeZero},n]$. Phase space is the product of configuration and momentum fields on the periodic lattice $\mathbb{Z}/n\mathbb{Z}$. The Poisson bracket is the standard sum $\sum_i(\partial_{q_i}F,\partial_{p_i}G-\partial_{p_i}F,\partial_{q_i}G)$.
The dynamic Hamiltonian $H_N^{\mathrm{dyn}}$ has unweighted kinetic slots and stiffness weighted by the structure factor $g_j=1+q_j^2$ (equivalently the inverse-metric factor). Momentum partials are simply $N_j p_j$. Configuration partials carry the frozen HamW-style bond terms plus an explicit $\partial g/\partial q$ correction $N_j q_j(\Delta q_j)^2$.
The module doc records the target identity: structure factor sits at the left split point $j$, matching the $n=2$ placement, with no boundary term because ZMod wraparound is periodic.
proof idea
Unfold the Poisson bracket definition and substitute the closed forms of the configuration and momentum partials of $H_N^{\mathrm{dyn}}$ and $H_M^{\mathrm{dyn}}$. The resulting sum still contains the $\partial g/\partial q$ correction pieces.
A single Finset.sum_congr step with ring shows those corrections cancel sitewise, leaving only the antisymmetric lapse combination $(N_{j-1}M_j-M_{j-1}N_j)$ times $(1+q_{j-1}^2),p_j(q_j-q_{j-1})$.
Finally apply the periodic reindex lemma sum_reindex by one lattice step (using $j+1-1=j$) to shift indices so the structure factor sits at the left split point $j$ and the sum matches the claimed RHS.
why it matters
This is the headline exact dynamic structure-function identity at general $n$. Downstream, bracket_HamDynN_HamDynN' rewrites it with the named inverse-metric factor, and bracket_HamDynN_recovers_bracket_HamDyn checks consistency with the original two-site theorem.
In Dirac-algebra continuum binding, bracket_HamDynN_eq_periodicSampled unfolds this identity at continuum samples to equate the lattice bracket with the periodic sampled dynamic bracket sum. That step is the bridge from discrete hypersurface deformation algebra toward continuum Dirac structure.
Within the Seven Gaps gravity program it closes the Frechet bookkeeping pattern (HamDynD, $\partial g/\partial q$ correction, Kronecker collapse, periodic reindex) for arbitrary $n$, so the dynamic structure factor is no longer a two-site special case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.