zeroMomDensity2
plain-language theorem explainer
Constant-zero momentum density on the two-site lattice phase space, independent of configuration and site. It is the decoy momentum field used to inhabit the weak point-split HKT schema while failing the strong load-bearing momentum gate. The definition is the constant real zero; downstream lemmas reduce brackets and differentiability to the zero functional.
Claim. On the two-site phase space (configuration and conjugate momentum maps $Z/2Z\to\mathbb{R}$), the vanishing momentum density at any phase-space point and any site index is the constant $0\in\mathbb{R}$.
background
The ambient setting is the Wave C2 repair of the point-split HKT target. An adversarial pass showed the weak dynamical target is decoy-inhabitable by a quartic Hamiltonian with identically zero momentum; rigidity over that weak class is therefore not load-bearing. This module strengthens the target with load-bearing momentum, Mom–Ham advection, and kinetic regularity, and exhibits an explicit quartic zero-momentum witness that passes the weak schema and fails the strong one.
Phase space for $n$ sites is the product of configuration and conjugate momentum maps $Z/nZ\to\mathbb{R}$. The sibling decorative structure $1+q_j^2$ mirrors the honest structure density used in the weak target. The continuum bridge identifies discrete Laplacian action with a weighted sum of squared site differences; here only the discrete two-site phase space is needed.
The zero density is the momentum half of that decoy: every weighted sum of sitewise values is the zero functional on phase space.
proof idea
Pure definition: ignore the phase-space point and site index and return the real constant $0$. No lemmas or tactics. Downstream, zeroMom2_eq_zero funexts and simplifies weighted sums to the constant-zero map; differentiability and Poisson brackets then collapse by rewriting to that identity.
why it matters
This is the momentum field of quarticZeroMomTarget, the formal witness that the weak point-split dynamical schema is decoy-inhabitable. It feeds zeroMom2_eq_zero, differentiable_zeroMom2, and bracket_zeroMom2_any, which together prove that every Mom–Mom bracket built from it vanishes. That vanishing is exactly what quarticZeroMom_fails_mom_load_bearing uses to exclude the decoy from the strong class.
In the module narrative, discrimination is: honest inhabitant passes, quartic zero-momentum decoy fails. Strong-class rigidity for the old point-split target is dead; binding rigidity moves to the canonical-momentum target. No ledger flag flips. The definition is scaffolding for that exclusion gate, not a physical momentum law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.