vacuumKineticLocalProfile
plain-language theorem explainer
The vacuum kinetic local Hamiltonian density is the quadratic-in-momentum profile A(a) p² + W(a,b), with A(a)=(1+a²)⁻¹ and W a fixed sextic polynomial in the field pair (a,b). HKT-rigidity and gap-5 workers cite it as the smooth kill inhabitant that breaks mod-vacuum rigidity. The definition is a direct pointwise assembly of those two coefficient maps into a three-argument local profile.
Claim. Define the local Hamiltonian profile $H:\mathbb{R}^{3}\to\mathbb{R}$ by $H(a,b,p)=A(a)\,p^{2}+W(a,b)$, where $A(a)=(1+a^{2})^{-1}$ and $W(a,b)=a^{6}/24+7a^{4}/24-a^{3}b^{3}/6-a^{3}b/2+a^{2}b^{4}/8+a^{2}b^{2}/4+a^{2}/4-ab^{3}/6-ab/2+b^{4}/8+b^{2}/4$.
background
Module setting is Wave C4/C5 gap 5: mod-vacuum kill plus kinetic-normalized rigidity. A local Hamiltonian profile is simply a map $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, read as density in field value $a$, conjugate $b$, and momentum $p$.
The kinetic prefactor $A(a)=(1+a^{2})^{-1}$ is positive and smooth. The potential piece $W(a,b)$ is the explicit polynomial fixed by the design of the variable-kinetic CanonicalMom inhabitant. Together they form the density that, once summed over the two-site $\mathbb{Z}/2$ lattice with site weights, supplies the Hamiltonian used to refute mod-vacuum rigidity.
Upstream, the profile type is the bare three-argument function space; the two coefficient maps are pure definitions with no further hypotheses.
proof idea
Pure definitional assembly: the profile is the lambda $(a,b,p)\mapsto A(a)\cdot p^{2}+W(a,b)$. No lemmas, no tactics, no rewriting. Downstream equalities (exact-cost chart, per-site jet) recover this same pointwise formula by funext and ring or quadratic unfolding.
why it matters
This is the concrete kill inhabitant for gap 5. Downstream, it equals the exact-cost kinetic profile at chart $\lambda=1/2$ with weights $2A(a)$, so deleting the composition-law clause readmits the target that refutes mod-vacuum rigidity. It likewise equals the per-site jet profile at $\kappa=1$. The companion exclusion theorem shows no composition-law-certified presentation exists in any chart: the law forces unit weight, then two field values disagree on the coefficient.
Inside the same module it feeds differentiability of the summed Hamiltonian, the Poisson-bracket identity ham_ham_vacuumKinetic, and the derivative lemmas in $b$ and $p$. Those facts underwrite the kinetic-normalized CanonicalMom intensivity field and the theorem-derived FTC recovery that closes the C5 ledger half. Framework role is local to the HKT seven-gaps gravity stack, not a T0–T8 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.