bracket_quarticHam2_quarticHam2
plain-language theorem explainer
On the two-site lattice phase space, the Poisson bracket of any two weighted quartic Hamiltonians vanishes identically. Gravity and HKT rigidity work cite this when excluding pure-configuration quartics from load-bearing dynamics. The proof is a short term argument: q-partials of the quartic Hamiltonian are zero, so every summand in the bracket is algebraically zero.
Claim. Let $N,M:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ be site weights and let $x$ be a point of the two-site phase space $(q,\pi)$. Write $H_N^{(4)}(x)=\sum_j N(j)\,\rho^{(4)}(x,j)$ for the weighted quartic Hamiltonian density sum. Then the Poisson bracket satisfies $\{H_N^{(4)},H_M^{(4)}\}(x)=0$.
background
Phase space here is the canonical lattice model: configuration $q$ and conjugate momentum $\pi$, each a real function on the periodic two-site lattice $\mathbb{Z}/2\mathbb{Z}$. Observables are real functions of $(q,\pi)$. The Poisson bracket is the standard sum over sites of $\partial_q F,\partial_\pi G-\partial_\pi F,\partial_q G$, with partials realized via Fréchet derivatives (junk zero when nondifferentiable).
The quartic Hamiltonian is a linear combination, with site weights $N$, of a fixed quartic density on each site. An upstream lemma records that every configuration partial of this Hamiltonian vanishes identically: the density depends on momenta (and the weighted sum inherits that).
This module is the Wave C2 repair after an adversarial pass showed the weak point-split HKT target is decoy-inhabitable by a quartic zero-momentum package. The strong target adds load-bearing momentum and honest advection; the weak schema still admits the quartic decoy as a formal witness.
proof idea
Unfold the Poisson bracket definition and rewrite every configuration partial via the lemma that $\partial_{q_j}H_N^{(4)}=0$ at every site and every phase-space point. Each summand then reduces to $0\cdot(\cdots)-(\cdots)\cdot 0$. Finish by Finset.sum_eq_zero and a one-line ring on the zero product. No differentiability side conditions are needed because the partial lemma already supplies the concrete zero values used by the total bracket.
why it matters
This identity is the algebraic engine behind the quartic zero-momentum decoy: that package inhabits the weak point-split dynamical schema and is the formal witness that weak rigidity is not load-bearing. Downstream, the same vanishing is reused (after a density equality) for the balanced-quartic Hamiltonians in the CanonicalMom target module, where the balanced-quartic falsifier kills strong-class rigidity and moves the binding grind to CanonicalMom.
In the SevenGaps gravity stack this is bookkeeping for hypersurface-deformation / HKT-style structure, not a new physical constant. It closes the decoy side of the discrimination gate (honest inhabitant passes, quartic zero-momentum fails the strong class via momentum load-bearing) without flipping any ledger flag. Framework landmarks T0–T8 are not directly invoked; the result is local to the lattice Poisson calculus used by the HKT point-split targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.