bracket_quarticBalancedHam_quarticBalancedHam
plain-language theorem explainer
On the two-site phase space, the Poisson bracket of any two balanced-quartic Hamiltonians vanishes pointwise. Gravity workers building HKT point-split targets cite this to certify that the balanced quartic Hamiltonian sector is abelian. The proof identifies the balanced Hamiltonian with the ordinary quartic one (identical kinetic densities) and reuses the already-proved ordinary quartic bracket identity.
Claim. For every pair of lapse functions $N,M:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and every point $x$ of the two-site phase space, the Poisson bracket of the balanced-quartic Hamiltonians built from $N$ and $M$ vanishes: $\{H^{\mathrm{bal}}_N,H^{\mathrm{bal}}_M\}(x)=0$.
background
Module setting is Wave C2 gap5 of the SevenGaps gravity ledger: inhabit a weak HKT point-split target with a balanced quartic model, separate it from the strong-rigidity claim, and leave the CanonicalMom rigidity statement DEFINED-only for later sessions. No ledger flag is flipped.
The Poisson bracket on phase space is the standard sum ${F,G}(x)=\sum_i(\partial_{q_i}F,\partial_{p_i}G-\partial_{p_i}F,\partial_{q_i}G)$. The balanced-quartic Hamiltonian density is the pure kinetic model $\pi_j^4$ on each of the two sites; the integrated Hamiltonian is the lapse-weighted sum of those densities. The ordinary (non-balanced) quartic Hamiltonian uses exactly the same density $\pi_j^4$, so the two Hamiltonian functionals coincide as maps on phase space. What differs in the balanced model is the momentum density and structure function (load-bearing $m_j=(\pi_0+\pi_1)\cdot\mathrm{structure}(x,j+1)$ with a balance identity that cancels the ham-ham right-hand side on $\mathbb{Z}/2\mathbb{Z}$).
Upstream, bracket_quarticHam2_quarticHam2 already shows that any two ordinary quartic Hamiltonians Poisson-commute, by reducing the bracket to a sum that rings to zero after the $q$-derivatives of the quartic kinetic term vanish.
proof idea
Two short equalities of functionals, then a rewrite. First prove pointwise that the balanced-quartic Hamiltonian equals the ordinary quartic Hamiltonian for the same lapse $N$, by funext and simp on the shared density $\pi_j^4$. Repeat for $M$. Then simpa rewrites the goal to the upstream theorem that the ordinary quartic Hamiltonians Poisson-commute, and apply that theorem at $(N,M,x)$. No fresh differentiation is performed here.
why it matters
Feeds the balanced-quartic weak target: the downstream package quarticBalancedWeakTarget assembles ham/mom densities, structure function, and advector fields into an inhabitant of the weak point-split schema HKTPointSplitTargetDyn 2. Vanishing of the ham-ham bracket is the abelian Hamiltonian-sector half of that schema; without it the balanced model could not serve as a counterexample to strong rigidity while still sitting inside the weak target.
In the binding design this is Session B material: exhibit an honest HamDyn inhabitant, separate the balanced quartic from the CanonicalMom class, and bank the DEFINED-only CanonicalMom rigidity statement for sessions C. It does not touch the Recognition forcing chain (T0-T8) or the RCL directly; it is local to the HKT hypersurface-deformation algebra used in the gravity SevenGaps program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.