not_HKTRigidityStatement_one
plain-language theorem explainer
The Hojman–Kuchař–Teitelboim rigidity claim fails at lattice size one: a quartic one-site Hamiltonian density sits in the target class yet is not of the form c_kin π² + c_vac. Anyone tracking Gap 5 constraint recovery or the kill-tower scope certificate cites this. The proof evaluates the forced quadratic form at three constant momenta and obtains 16 = 4.
Claim. The rigidity statement for the Hojman–Kuchař–Teitelboim target on a one-site lattice is false: there exist coefficients and a Hamiltonian density in that target class whose on-site values are not of the form $c_{\mathrm{kin}}\,\pi^2 + c_{\mathrm{vac}}$ for any fixed real $c_{\mathrm{kin}}, c_{\mathrm{vac}}$.
background
Gap 5 in the Seven Gaps gravity program concerns whether the Hojman–Kuchař–Teitelboim (HKT) hypersurface-deformation algebra forces the Hamiltonian density into the Einstein–Hilbert quadratic pin. The rigidity statement asserts that every density in the target class is of the shape $c_{\mathrm{kin}}\pi^2 + c_{\mathrm{grad}}(\nabla q)^2 + c_{\mathrm{vac}}$.
On the degenerate lattice $\mathbb{Z}/1\mathbb{Z}$ every discrete difference vanishes identically ($j+1=j$), so the gradient slot is zero. The module constructs a constant-configuration phase point momPoint p with momentum $p$ at the unique site, and a quartic kinetic density $\pi^4$ with vanishing momentum density. That pair inhabits the one-site HKT target while escaping the quadratic pin.
Codex adjudication recorded that the unconditioned rigidity claim is false as stated; this module lands the counterexample against the real Fréchet-derivative Poisson bracket without flipping the Gap 5 recovery flag.
proof idea
Assume the rigidity statement at $n=1$ and apply it to the quartic one-site HKT inhabitant. The resulting form identity, specialized at momPoint p and simplified by momPoint_p, momPoint_q, zmod1_add_self, sub_self, mul_zero, and add_zero, collapses to
$$p^4 = c_{\mathrm{kin}},p^2 + c_{\mathrm{vac}}$$
for every real $p$ (gradient term gone).
Evaluate at $p=0$ to force $c_{\mathrm{vac}}=0$; at $p=1$ to force $c_{\mathrm{kin}}=1$; at $p=2$ to obtain $16=4$, contradiction.
why it matters
This is the headline one-site falsification for Wave C2 R5/R6 groundwork. Downstream it is the first conjunct of gap5_kill_tower_scope_certificate, which packages four not_* theorems as a scope certificate that stronger unconditioned rigidity statements fail. It also closes the typed residual typedResidual_gap5_hkt_one_site_falsification_closed in the Gap 5 residual DAG (Wave D: frozen HKT rigidity at $n=1$ falsified).
The ledger terminal that would pin general relativity to HKT must therefore bind to a repaired statement (dynamic variant, or $n$-restricted nondegenerate form), with this counterexample disclosed. The module explicitly does not flip gap5_constraint_recovery and does not prove any positive rigidity theorem. In the broader RS gravity stack this keeps Gap 5 honest: the quadratic pin is not free at degenerate lattice size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.