differentiable_zeroMom
plain-language theorem explainer
On the one-site phase space, the smeared vanishing momentum density is differentiable for every weight function. Anyone building the n=1 HKT counterexample cites this to fill the momentum-differentiability field. The proof rewrites the smeared map to the constant zero function and applies constant differentiability.
Claim. For every weight $w:\mathbb{Z}/1\mathbb{Z}\to\mathbb{R}$, the map $x\mapsto\sum_{j} w(j)\,\mu_0(x,j)$ on the one-site phase space $(\mathbb{Z}/1\mathbb{Z}\to\mathbb{R})^2$ is differentiable over $\mathbb{R}$, where $\mu_0$ is the identically zero momentum density.
background
The ambient setting is Wave C2 groundwork against HKT rigidity as stated: on the degenerate 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 Hojman–Kuchař–Teitelboim target at $n=1$ while escaping the quadratic pin.
Phase space is the product of configuration and conjugate momentum fields on the periodic lattice, here with a single site. The model momentum density is the constant zero function on that phase space. The smeared momentum is the weighted sum of that density against an arbitrary weight $w$.
An upstream identity already records that this smeared map equals the constant zero functional, which is the only algebraic input needed for differentiability.
proof idea
One short rewrite-and-close proof. Rewrite the smeared functional via the identity that it equals the constant zero map on phase space. Then apply the standard fact that constant maps are differentiable, instantiated at $0$.
why it matters
This lemma supplies the mom_differentiable field of the quartic one-site HKT inhabitant. That inhabitant is the concrete counterexample showing every real field of the Hojman–Kuchař–Teitelboim target at $n=1$ can hold for a non-quadratic Hamiltonian with identically zero momentum density.
It does not flip constraint recovery and does not prove any rigidity theorem. Its role is negative: force the ledger terminal that claims HKT pins general relativity to bind to a repaired statement (dynamical form, or $n$-restricted nondegenerate form), with this one-site escape disclosed. In the Seven Gaps gravity stack, it is scaffolding for an honest falsification of an over-strong design claim, not a positive GR derivation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.