bracket_HamDyn_shape
plain-language theorem explainer
On the two-site lattice, the Poisson bracket of two dynamic Hamiltonians equals a sum of discrete Wronskians of the lapses, each multiplied by the concrete dynamic inverse metric and the raw momentum-flux. Gravity workers in the seven-gap program cite this as the R1 structure-function shape under the continuum-module name. The proof is a one-line wrapper of the already-proved two-site dynamic bracket identity.
Claim. For lapses $N,M:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase point $x=(q,\pi)$ on the two-site phase space, the Poisson bracket of the dynamic Hamiltonians satisfies $\{H_N^{\mathrm{dyn}},H_M^{\mathrm{dyn}}\}(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}}(N_j M_{j+1}-M_j N_{j+1})\,(1+q_j^2)\,(\pi_{j+1}(q_{j+1}-q_j))$.
background
The ambient setting is Wave C2 R4 of the gravity seven-gap stack: packaging the sampled-lapse Wronskian rate-$h$ residual with the R2 lattice RHS shape and the R3 dynamic structure profile. Phase space is the product of configuration and momentum fields on a periodic lattice of $n$ sites; here $n=2$. The Poisson bracket is the standard sum $\sum_i(\partial_{q_i}F,\partial_{\pi_i}G-\partial_{\pi_i}F,\partial_{q_i}G)$.
The dynamic Hamiltonian $H_N^{\mathrm{dyn}}$ is the unfolded two-site energy with lapse $N$, kinetic $\pi_i^2$ and potential $(1+q_i^2)(\Delta q_i)^2$. The concrete dynamic inverse metric is the positive sitewise factor $G_j=1+q_j^2$. Upstream, the R1 headline identity already expands ${H_N^{\mathrm{dyn}},H_M^{\mathrm{dyn}}}$ into the discrete Wronskian times $G_j$ times the raw momentum-flux $\pi_{j+1}\Delta q_j$.
proof idea
One-line wrapper: the statement is definitionally identical to the upstream R1 theorem bracket_HamDyn_HamDyn, which itself unfolds by simp on the Poisson bracket and the partial derivatives of the dynamic Hamiltonian against the concrete inverse metric. No new algebra is performed here.
why it matters
This declaration re-exports the exact two-site dynamic structure-function identity into the continuum module so that the lattice RHS shape is available under the R4 naming. The module aims at a continuum limit of the form $n\sum\to\int(NM'-MN'),G,(p,q')$, with per-site scaling $O(1/n^2)$ and honest prefactor $n$ rather than $n^2$.
No downstream consumers are wired yet (used_by is empty). The freestanding ledger name for a full Dirac-algebra continuum limit remains held free: HamDyn exists only at $n=2$, and non-periodic mesh wraparound is undischarged. The result does not close gap-5 constraint recovery (needs R6) and is distinct from the frozen-$G=1$ decoy integrand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.