bracket_HamDynN_HamDynN_eq_two
plain-language theorem explainer
At two lattice sites, the Poisson bracket of a pair of general-n dynamic Hamiltonians equals the bracket of the original two-site dynamic Hamiltonians. Anyone reconnecting the general-n structure formula to the n=2 case cites this. The proof is a one-line rewrite through definitional equality of the two Hamiltonian families.
Claim. For lapse fields $N,M:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x$, the Poisson bracket of the general-$n$ dynamic Hamiltonians specialized to $n=2$ equals the Poisson bracket of the original two-site dynamic Hamiltonians: $\{\mathrm{Ham}_{\mathrm{dyn},N}^{(2)},\mathrm{Ham}_{\mathrm{dyn},M}^{(2)}\}(x)=\{\mathrm{Ham}_{\mathrm{dyn},N},\mathrm{Ham}_{\mathrm{dyn},M}\}(x)$.
background
The module generalizes the two-site dynamic structure bracket to arbitrary lattice size $n$ with $\mathrm{NeZero},n$. Configuration and momentum live on the periodic lattice phase space $(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})$. 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 original two-site Hamiltonian $\mathrm{HamDyn}$ has unweighted kinetic slot and stiffness slot weighted by $g_j=1+(q_j)^2$. The general-$n$ model $\mathrm{HamDynN}$ has the same shape summed over $\mathbb{Z}/n\mathbb{Z}$. Upstream, $\mathrm{HamDynN}$ at $n=2$ is definitionally equal to $\mathrm{HamDyn}$ (by rfl).
proof idea
One-line wrapper. Rewrite both Hamiltonian arguments of the bracket by the definitional equality that identifies the general-$n$ dynamic Hamiltonian at $n=2$ with the original two-site dynamic Hamiltonian; apply that equality once on each side.
why it matters
Closes the $n=2$ consistency gate in the Wave C2 R4 repair that lifts the dynamic structure bracket from two sites to general $n$. Downstream, the recovery theorem uses this identity to show that the general-$n$ bracket formula, specialized to $n=2$, reproduces the concrete two-site structure expression involving the dynamic inverse-metric factor. Without it, the general RHS $\sum_j(N_j M_{j+1}-M_j N_{j+1})\cdot((1+q_j^2),p_{j+1}(q_{j+1}-q_j))$ could not be certified as a true extension of the already-proved two-site bracket. It is pure scaffolding glue inside the gravity SevenGaps chain, not a new physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.