bracket_zeroMom_any
plain-language theorem explainer
On the one-site lattice, the hypersurface-deformation bracket of any weighted sum of zero momentum densities against an arbitrary phase-space functional is identically zero. Gravity workers auditing the Hojman–Kuchař–Teitelboim target fields cite this when checking algebra closure for a pure-momentum Hamiltonian with vanishing momentum density. The proof is a three-line reduction: expand the bracket, insert the vanishing Q- and P-partials, then sum zeros by ring.
Claim. For every weight $w:\mathbb{Z}/1\mathbb{Z}\to\mathbb{R}$, every functional $G$ on the one-site phase space, and every point $x$ in that phase space, the discrete hypersurface-deformation bracket satisfies $\{\sum_j w(j)\,\pi_0(\cdot,j),\,G\}(x)=0$, where $\pi_0$ denotes the identically zero momentum density.
background
This module builds an explicit counterexample to the Hojman–Kuchař–Teitelboim (HKT) rigidity claim as originally stated, restricted to the degenerate one-site lattice $\mathbb{Z}/1\mathbb{Z}$. On a single site every discrete difference and Wronskian vanishes, so a quartic kinetic density paired with identically zero momentum density can meet every field of the HKT target while escaping the quadratic pin.
The hypersurface-deformation bracket (from the HypersurfaceDeformation import) is the discrete Poisson-type pairing of two phase-space functionals, assembled from configuration and momentum partial derivatives. The zero momentum density is the constant-zero field on the one-site lattice. Upstream lemmas show that both its configuration partials and its momentum partials vanish at every site, by reducing the weighted sum to the zero functional and simplifying.
The present identity packages those vanishing partials into a bracket statement: any functional built as a weighted sum of zero momentum densities brackets to zero against every second argument.
proof idea
Expand the bracket definition, then rewrite the configuration and momentum partials of the weighted zero-momentum functional by the two vanishing-partial lemmas. Each summand of the resulting finite sum is an algebraic product that contains a zero factor, so the sum is identically zero by applying ring on each term and invoking the finite-sum-of-zeros lemma.
why it matters
The one-site HKT target inhabitant (quartic densities with zero momentum density) needs mixed brackets involving the momentum density to vanish. This lemma supplies that vanishing for an arbitrary second argument whenever the first argument is any weighted sum of zero momentum densities. Together with the quartic self-bracket identity and the collapse of discrete differences on $\mathbb{Z}/1\mathbb{Z}$, it completes the counterexample that falsifies HKT rigidity as stated for $n=1$.
Per the module adjudication note, the construction does not flip the gap-5 constraint-recovery claim and does not prove any repaired rigidity theorem. The ledger terminal that pins general relativity via Hojman-type arguments must bind to a repaired statement (dynamic form, or an $n$-restricted nondegenerate form), with this counterexample disclosed. This is Wave C2 groundwork in the Seven Gaps gravity program, not a step of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.