vacuumKinetic_nondeg
plain-language theorem explainer
The vacuum kinetic Hamiltonian density is nonzero at a concrete two-mode phase point: vanishing configuration and unit momentum on the first Z/2 slot. Authors of the kinetic-normalized HKT rigidity package cite this to discharge the nondegeneracy side-condition of the weak target. Proof is pure unfolding of the local profile followed by numerical evaluation.
Claim. Let the vacuum kinetic local profile be $H(a,b,p)=(1+a^2)^{-1}p^2+W(a,b)$ with the fixed polynomial potential $W$. On the two-component phase space, at the point with configuration $q\equiv 0$ and momentum $p_0=1$, $p_1=0$, the Hamiltonian density on component $0\in\mathbb{Z}/2\mathbb{Z}$ satisfies $H(q_0,q_1,p_0)\neq 0$.
background
Module setting is Wave C4/C5 gap5: mod-vacuum kill plus kinetic-normalized rigidity for the HKT (Hamiltonian kinetic target) package in the SevenGaps gravity ledger. The vacuum kinetic model supplies an explicit two-mode Hamiltonian density used as a concrete inhabitant of the kinetic-normalized canonical-momentum class.
The amplitude factor is $A(a)=(1+a^2)^{-1}$. The potential $W(a,b)$ is a fixed bivariate polynomial (degree six, with mixed $a^3b^3$, $a^2b^4$, etc. terms). The local profile is $A(a),p^2+W(a,b)$, and the density on component $j$ reads that profile at $(q_j,q_{j+1},p_j)$. The nondegeneracy phase point is the pure-momentum configuration $q\equiv 0$, $p=(1,0)$ on $\mathbb{Z}/2\mathbb{Z}$.
These defs sit alongside positivity of $A$ and the design identity for $W$; together they feed the weak dynamical target that packages ham/mom densities and structure functions for the rigidity PDE side.
proof idea
One-shot simplification. Unfold the density to the local profile, substitute the nondegeneracy phase (so $a=0$, $b=q_1=0$, $p=1$), expand $A$ and $W$, and reduce the $\mathbb{Z}/2$ index arithmetic $0+1=1$. The resulting rational expression collapses under norm_num to the nonzero constant $1$ (since $A(0)=1$ and $W(0,0)=0$). No external lemmas beyond the local arithmetic facts for $\mathbb{Z}/2$ addition.
why it matters
Feeds vacuumKineticWeakTarget, the concrete HKTPointSplitTargetDyn 2 that packages this ham density with the dynamical momentum density and structure function. That target is the kinetic-normalized half of the gap5 ledger: after the mod-vacuum kill (Part 1) rules out the rigid vacuum statement, Part 2 needs a nondegenerate kinetic model whose FTC recovery is theorem-derived rather than assumed.
In the Recognition gravity stack this closes a side-condition on the intensivity field for CanonicalMom rigidity. It does not itself touch the forcing chain T0–T8 or the RCL, but it is required infrastructure for the SevenGaps gravity adjudication binding (D-qg-hkt-modvacuum-verdict / D-gap5-acceptance-adjudication). Without nondegeneracy the weak target would be formally ill-posed for the subsequent PDE rigidity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.