bracket_zeroMom2_any
plain-language theorem explainer
Any weighted sum of the vanishing two-site momentum densities has identically zero Poisson bracket with every phase-space observable. HKT rigidity and decoy-exclusion arguments cite this to kill the quartic zero-momentum inhabitant of the weak point-split schema. The proof is a short tactic reduction: the density is the zero function, so all Q/P partials vanish and the bracket sum is zero.
Claim. For every weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, every real-valued observable $G$ on the two-site phase space, and every point $x$, the hypersurface Poisson bracket of the weighted zero-momentum density against $G$ vanishes: $\{\sum_{j} w(j)\,\rho^{\mathrm{mom}}_{0}(\cdot,j),\,G\}(x)=0$.
background
This module repairs the point-split HKT target after an adversarial pass showed the weak dynamical schema is decoy-inhabitable by a quartic zero-momentum model. The strong class adds load-bearing momentum (nonvanishing Mom–Mom brackets), advection tied to the Mom–Ham bracket calculus, and kinetic regularity. Discrimination: honest inhabitants pass; the quartic zero-momentum decoy fails.
The decoy momentum density zeroMomDensity2 is the constant-zero field on two-site phase space. Its weighted sum is therefore the zero observable (zeroMom2_eq_zero). The Poisson bracket here is the hypersurface deformation bracket: a sum over sites of Q- and P-directional Fréchet derivatives (pderivQ, pderivP).
Local setting is Wave C2 of the SevenGaps gravity stack: strengthen the point-split HKT target so rigidity claims are not grindable against a free decoy, then move binding rigidity to the CanonicalMom target.
proof idea
Invoke zeroMom2_eq_zero to replace the weighted density by the constant-zero function. Unfold bracket into the sum of Q- and P-partials. For each site index, the Fréchet derivative of the zero function along both $(e_i,0)$ and $(0,e_i)$ is zero (rewrite by the identity, then simp). Finish with Finset.sum_eq_zero and simplify each summand by those vanishing partials. No nontrivial bracket algebra is needed: vanishing of the first argument forces the whole bracket to zero for arbitrary second argument $G$.
why it matters
Parent use is quarticZeroMom_fails_mom_load_bearing, which states that the zero-momentum decoy has identically vanishing Mom–Mom brackets and is therefore excluded from the strong class by the load-bearing momentum field. The same fact underwrites the decoy package quarticZeroMomTarget (weak-schema inhabitant with momDensity := zeroMomDensity2), the formal witness of critic finding D-qg-hkt-pointsplit-adjudication-20260722.
In the Recognition gravity stack this is a discrimination gate, not a physics prediction: it certifies that the weak point-split HKT schema is too loose, so strong-class rigidity is dead and binding rigidity moves to HKTCanonicalMomTarget. No ledger flag flips; the lemma only closes the decoy-exclusion half of the Wave C2 repair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.