zeroMomDensity
plain-language theorem explainer
Constant-zero momentum density on the one-site lattice phase space. Anyone building or citing the HKT one-site counterexample uses it as the momentum-density field that pairs with the quartic kinetic density. The body is the literal constant 0, so every smeared sum, partial, and Poisson bracket involving it collapses immediately.
Claim. On the one-site canonical phase space (configuration and conjugate momentum maps $Z/1Z\to\mathbb{R}$), the momentum density at every phase-space point and every lattice index equals $0$.
background
The ambient module constructs an explicit counterexample to the Hojman–Kuchař–Teitelboim rigidity claim as originally stated, restricted to the degenerate one-site lattice $Z/1Z$. On that lattice every discrete difference and Wronskian vanishes, so a quartic kinetic density together with a vanishing momentum density can satisfy every field of the HKT target while escaping the quadratic pin.
Phase space here is the product of configuration and conjugate-momentum maps on $n$ periodic sites; for $n=1$ both factors are maps $Z/1Z\to\mathbb{R}$. Momentum density is the local density that, after smearing against a weight, enters the Poisson bracket and the HKT target structure. This definition supplies the identically zero choice of that density.
Upstream, the phase-space abbreviation and the hypersurface-deformation bracket infrastructure fix the ambient calculus; the present constant is the simplest density compatible with that calculus on one site.
proof idea
Definitional constant: the body is the real number 0, ignoring both the phase-space argument and the site index. No lemmas are applied. Downstream lemmas such as zeroMom_eq_zero, the configuration and momentum partials, differentiability, and the smeared bracket all reduce by unfolding this constant and simplifying.
why it matters
This density is the momentum-density field of quarticOneSiteHKT, the inhabitant that witnesses every real field of HojmanKucharTeitelboimTarget 1. Downstream lemmas (zeroMom_eq_zero, differentiable_zeroMom, pderivQ_zeroMom, pderivP_zeroMom, bracket_zeroMom_any) all rest on it: smeared sums are identically zero, partials vanish, and the Poisson bracket against any observable is zero.
In the Seven Gaps gravity program this is Wave C2 groundwork for R5/R6. It does not flip gap5_constraint_recovery and does not prove any repaired rigidity theorem. It forces the ledger terminal hojman_pins_general_relativity to bind to a corrected statement (dynamic or n-restricted nondegenerate form), with the one-site counterexample disclosed. Framework-wise it is local to the discrete HKT analysis, not to the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.