zeroMom2_eq_zero
plain-language theorem explainer
Any weighted sum of the vanishing momentum density on the two-site phase space is the zero functional. HKT point-split and decoy-discrimination proofs cite it to discharge bracket and differentiability side conditions for the quartic zero-momentum decoy. The argument is function extensionality plus unfolding the constant-zero density.
Claim. For every weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the map $x\mapsto\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\,\rho_0(x,j)$ on the two-site phase space equals the zero function, where $\rho_0$ is the vanishing momentum density (identically zero).
background
The module repairs the point-split HKT target after an adversarial pass showed the weak dynamical schema is decoy-inhabitable by a quartic zero-momentum construction. Phase space for $n$ sites is the product of configuration and conjugate-momentum fields on the periodic lattice $\mathbb{Z}/n\mathbb{Z}$; here $n=2$.
The vanishing momentum density is the constant-zero model density used as that decoy. Weighted sums of it appear as candidate momentum observables. The strong class adds load-bearing momentum, Mom–Ham bracket advection, and kinetic regularity so the decoy is excluded while an honest Hamiltonian-advection inhabitant still passes.
proof idea
Term proof: function extensionality at an arbitrary phase-space point, then simp with the definition of the vanishing momentum density. That density is the constant map $0$, so every weighted sum collapses to the zero real immediately.
why it matters
Feeds two local side conditions on the decoy momentum observable: its Poisson bracket against any functional vanishes, and the weighted sum is differentiable (as a constant). Those lemmas support the discrimination gate that separates the honest Hamiltonian-advection inhabitant from the quartic zero-momentum decoy.
In the broader Wave C2 story, strong-class rigidity for the point-split target is already false (balanced-quartic falsifier); binding rigidity moves to the canonical-momentum target. This lemma is pure bookkeeping that makes the decoy witness formally usable in bracket calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.