bracket_HamDynN_HamDynN'
plain-language theorem explainer
Equivalent rewrite of the general-$n$ dynamic structure-function identity: the Poisson bracket of two dynamic Hamiltonians equals a cyclic sum whose structure weight is the named inverse-metric factor $1+q_j^2$. Gravity workers citing the Hamiltonian–Hamiltonian bracket at arbitrary lattice size use this form when they want that factor named rather than expanded. Proof is a one-line `simpa` off the expanded headline identity.
Claim. Let $N,M:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and let $x=(q,p)$ be a point of the $n$-site phase space. Writing $H_N^{\mathrm{dyn}}$ for the dynamic Hamiltonian with unweighted kinetic slot and stiffness weight $1+q_i^2$, and writing $g_j(x):=1+q_j^2$ for the dynamic inverse-metric factor, one has $\{H_N^{\mathrm{dyn}},H_M^{\mathrm{dyn}}\}(x)=\sum_j(N_j M_{j+1}-M_j N_{j+1})\,g_j(x)\,(p_{j+1}(q_{j+1}-q_j))$.
background
This module (Wave C2 R4 repair, Step 2) lifts the two-site dynamic structure bracket from $n=2$ to arbitrary $n$ with a nonzero modulus. Phase space is the product of configuration and momentum fields indexed by $\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 kinetic term unweighted and stiffness slot carrying the structure factor $g_i=1+q_i^2$, matching the two-site model. The named factor dynamicInverseMetricN is exactly $g_j(x)=1+(q_j)^2$, placed at the left split point of each bond, the same placement used by the background weight in the weighted Hamiltonian.
Upstream, the expanded identity already states the same RHS with $1+q_j^2$ written out; the two-site theorem is the $n=2$ special case with the concrete inverse metric.
proof idea
One-line wrapper. Apply the expanded headline identity bracket_HamDynN_HamDynN, then simpa with the definition of the dynamic inverse-metric factor and pow_two so that $1+(q_j)^2$ matches $1+q_j\cdot q_j$. No new calculus.
why it matters
Gives the citation-friendly form of the general-$n$ dynamic structure-function identity: structure weight packaged as the named inverse-metric factor rather than an inline polynomial. The module doc records the true RHS derived from the Fréchet bookkeeping (partial-$g$ corrections cancel in the Hamiltonian–Hamiltonian bracket; ZMod wraparound contributes no boundary term). Downstream consistency note: at $n=2$ this recovers the two-site R1 headline. Sits in the Seven Gaps gravity stack as the general-lattice structure bracket used when building hypersurface-deformation algebra at arbitrary site count. No open scaffold: status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.