zeroMom_eq_zero
plain-language theorem explainer
On the one-site lattice, any smeared zero-momentum density is the zero functional on phase space. Gravity and HKT-counterexample work cite it to collapse partials and differentiability of the vanishing momentum sector. The proof is a one-line funext plus simp on the constant-zero density.
Claim. For every weight $w:\mathbb{Z}/1\mathbb{Z}\to\mathbb{R}$, the map $x\mapsto \sum_{j\in\mathbb{Z}/1\mathbb{Z}} w(j)\,\pi^{\mathrm{zero}}(x,j)$ on the one-site phase space equals the constant function $0$.
background
The ambient setting is Wave C2 groundwork against Hojman–Kuchař–Teitelboim rigidity: on the degenerate one-site lattice $\mathbb{Z}/1\mathbb{Z}$, discrete differences and Wronskians vanish, so a quartic kinetic density paired with zero momentum can meet every field of the HKT target while escaping the quadratic pin.
Phase space for $n$ sites is the product of configuration and conjugate momentum fields $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=1$. The model density zeroMomDensity is the constant zero function on that phase space (vanishing momentum density). Smearing against an arbitrary weight $w$ therefore produces a candidate momentum observable that should be identically zero.
This lemma records that identity of functionals, so later derivative and differentiability facts can rewrite through the constant map rather than manipulate the sum.
proof idea
Term-mode proof by functional extensionality: fix an arbitrary phase-space point $y$, then simp with the definition of the vanishing momentum density, which is the constant $0$. The weighted sum collapses to $0$ at every point, so the two functions agree.
why it matters
The lemma is local plumbing inside the HKT one-site counterexample module. Downstream, differentiable_zeroMom rewrites through it and applies differentiability of constants; pderivQ_zeroMom and pderivP_zeroMom likewise rewrite and simplify partials in $q$ and $\pi$ to zero. Those facts feed the real-fderiv Poisson bracket side of the counterexample: a quartic Hamiltonian density with zero momentum density can satisfy the HKT target fields on $n=1$ while escaping the quadratic pin.
Per the module doc, this does not flip gap5_constraint_recovery and does not prove any positive rigidity theorem. It supports disclosing that HKTRigidityStatement is false as stated, so the ledger terminal hojman_pins_general_relativity must bind to a repaired form (dynamic or $n$-restricted nondegenerate).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.