bracket_quarticHam_quarticHam
plain-language theorem explainer
The Poisson bracket of two smeared quartic Hamiltonians vanishes at every point of the one-site phase space. Builders of the HKT one-site counterexample cite this to discharge the Hamiltonian self-bracket field. The proof unfolds the bracket, inserts vanishing configuration partials, and rings the finite sum to zero.
Claim. For any smearing maps $N,M:\mathbb{Z}/1\mathbb{Z}\to\mathbb{R}$ and any point $x$ of the one-site lattice phase space, the Poisson bracket of the two smeared quartic Hamiltonians is zero: $\{H_N^{\mathrm{quartic}},H_M^{\mathrm{quartic}}\}(x)=0$.
background
This module supplies a concrete counterexample showing that the stated Hojman–Kuchař–Teitelboim rigidity claim fails on the degenerate one-site lattice $\mathbb{Z}/1\mathbb{Z}$. On that lattice every discrete difference and Wronskian vanishes, so a pure quartic kinetic density with zero momentum density can satisfy every field of the HKT target while escaping the quadratic pin.
Phase space is the product of configuration and conjugate momentum maps on the periodic lattice. 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)$, with partials realized by Fréchet derivatives (junk value $0$ when nondifferentiable). The smeared quartic Hamiltonian is $\sum_j N(j),q_j^4$-style density in momentum; its configuration partials vanish identically by the upstream lemma on those partials.
proof idea
Term-mode, three lines. Unfold the Poisson bracket definition and rewrite every configuration partial of a smeared quartic Hamiltonian by the lemma that those partials are identically zero. The resulting sum is a sum of products each containing a zero factor; Finset.sum_eq_zero plus ring closes the identity at every lattice site.
why it matters
This identity is the self-bracket discharge inside the inhabitant quarticOneSiteHKT, which packages quartic kinetic density and zero momentum density as a full HojmanKucharTeitelboimTarget 1. That inhabitant is the explicit witness that HKT rigidity, as originally stated, is false on $n=1$. The module does not flip the ledger terminal on constraint recovery and does not prove any repaired rigidity theorem; it forces the terminal to bind to a dyn/nondegenerate restatement with this counterexample disclosed. In the Seven Gaps gravity chain it is local groundwork (Wave C2 R5/R6), not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.