vacuumKinetic_fails_modVacuum_hamShape
plain-language theorem explainer
The variable-kinetic Hamiltonian density cannot be rewritten in the mod-vacuum shape with nonzero kinetic and gradient coefficients plus a local potential of configuration alone. HKT rigidity auditors cite this when killing the N=2 mod-vacuum rigidity claim. The proof specializes to coincident phases, forces the potential to vanish, then reads off inconsistent kinetic prefactors at two configurations.
Claim. There do not exist nonzero $c_{\mathrm{kin}}, c_{\mathrm{grad}} \in \mathbb{R}$ and a map $V:\mathbb{R}\to\mathbb{R}$ such that for every two-site phase-space point $x$ and every site $j\in\mathbb{Z}/2\mathbb{Z}$, the vacuum-kinetic Hamiltonian density equals $c_{\mathrm{kin}}\,p_j^2 + c_{\mathrm{grad}}\,S(x,j)\,(\Delta q_j)^2 + V(q_j)$, where $S$ is that target's structure function and $\Delta q_j = q_{j+1}-q_j$.
background
Module setting is Wave C4/C5 gap5: kill the mod-vacuum HKT rigidity statement on N=2, then install a kinetic-normalized positive terminal. Binding notes name the mod-vacuum verdict and the later C5 acceptance adjudication. Part 1 of the module builds a variable-kinetic CanonicalMom inhabitant that refuses the mod-vacuum ham-density template.
Phase space here is two configuration coordinates $q$ and two momenta $p$, indexed by $\mathbb{Z}/2\mathbb{Z}$. The vacuum-kinetic target supplies a Hamiltonian density built from a configuration-dependent kinetic prefactor (sibling vacuumKineticA), a structure weight, and no free local potential of the mod-vacuum form. The mod-vacuum shape under test is exactly constant kinetic term plus constant times structure times squared nearest-neighbor jump plus $V(q_j)$ only.
Coincident-phase test points set neighboring configurations equal so gradient squares vanish, isolating the pure kinetic-plus-potential slice of the density identity.
proof idea
Assume $c_{\mathrm{kin}}$, $c_{\mathrm{grad}}$, $V$ exist with both coefficients nonzero and the density identity holding everywhere. Restrict to coincident-phase points (neighboring $q$ equal) at site $0$: structure-gradient terms drop, leaving $\mathrm{A}(q),p^2 = c_{\mathrm{kin}},p^2 + V(q)$.
Set $p=0$ to conclude $V(q)=0$ for all $q$. Specialize again at $(q,p)=(0,1)$ and $(1,1)$: the identity collapses to $\mathrm{A}(0)=c_{\mathrm{kin}}$ and $\mathrm{A}(1)=c_{\mathrm{kin}}$. Unfolding the kinetic prefactor gives $1$ versus $1/2$, contradiction by norm_num.
The gradient coefficient is never needed after the coincident reduction; nonvanishing of $c_{\mathrm{kin}}$ is what the two-point mismatch kills.
why it matters
This is the concrete obstruction half of Part 1 in the gap5 module: the variable-kinetic CanonicalMom counterexample does not sit inside the mod-vacuum ham-density shape, so it witnesses failure of the N=2 mod-vacuum rigidity statement. Module doc ties the work to the Codex cross-family binding D-qg-hkt-modvacuum-verdict-20260723 and the later C5 upgrade that derives FTC recovery rather than assuming it as a class field.
No downstream consumers are wired yet in the graph (used_by empty). The logical parent is the package claim $\neg$ mod-vacuum rigidity on two sites; after both ledger halves bind green, Gap5ConstraintCloseStatus owns the flip of gap5_constraint_recovery. In the broader RS gravity stack this is bookkeeping that a naive ultralocal-plus-local-potential template cannot absorb the variable-kinetic sector, clearing the path to the kinetic-normalized positive terminal in §4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.