pderivQ_quarticHam
plain-language theorem explainer
On the one-site phase space, every configuration partial of the smeared quartic Hamiltonian vanishes. Anyone building the HKT one-site counterexample cites this to kill the q-legs of the Poisson bracket. The proof rewrites the partial via the known Fréchet derivative, expands the derivative as a sum of pure momentum covectors, and collapses each summand.
Claim. For any smear $N:\mathbb{Z}/1\mathbb{Z}\to\mathbb{R}$, any site $j$, and any phase-space point $x$, the configuration partial of the smeared quartic Hamiltonian satisfies $\partial_{q_j} H_4[N](x)=0$.
background
This module builds an explicit counterexample to the Hojman–Kuchař–Teitelboim rigidity claim as stated, on the degenerate one-site lattice $\mathbb{Z}/1\mathbb{Z}$. Every discrete difference and Wronskian vanishes there, so a quartic kinetic density with zero momentum density can meet every field of the HKT target while escaping the quadratic pin.
The smeared quartic Hamiltonian is $H_4N=\sum_j N_j,p_j^4$. Its Fréchet derivative at $x$ is the continuous linear map $\sum_i N_i\cdot(4 p_i^3),\mathrm{d}p_i$, a pure momentum covector (no $\mathrm{d}q$ legs). Configuration and momentum partials are extracted from that Fréchet derivative by pairing against the coordinate projections.
The Poisson bracket on phase space is the standard sum ${F,G}=\sum_i(\partial_{q_i}F,\partial_{p_i}G-\partial_{p_i}F,\partial_{q_i}G)$, with the honest total convention that nondifferentiable points contribute the junk value $0$.
proof idea
Unfold the configuration partial as the Fréchet derivative of $H_4[N]$ paired against the $q_j$ coordinate direction. Replace that derivative by the explicit map quarticHamD via hasFDerivAt_quarticHam. After applying the continuous-linear sum, each summand is a scalar multiple of the momentum coordinate functional coordP i. Pairing a pure $\mathrm{d}p$ covector against a pure $\mathrm{d}q$ direction is zero, so simp [coordP] finishes the finite sum.
why it matters
Parent theorem bracket_quarticHam_quarticHam applies this twice: both generators depend only on momentum, so every configuration partial is zero and the full Poisson bracket collapses by ring. That vanishing bracket is the algebraic heart of the one-site HKT counterexample: a quartic kinetic generator closes under the hypersurface-deformation algebra without being quadratic.
In the Seven Gaps gravity program this is Wave C2 groundwork (R5/R6). It falsifies HKTRigidityStatement as written on $n=1$, without flipping gap5_constraint_recovery or proving any repaired rigidity theorem. The ledger terminal that claims HKT pins general relativity must bind to a strengthened statement (dynamical or $n$-restricted nondegenerate form) and disclose this counterexample. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is pure finite-dimensional symplectic algebra on a degenerate lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.