ham_ham_vacuumKinetic
plain-language theorem explainer
The Poisson bracket of two smearings of the vacuum-kinetic Hamiltonian density on the two-site phase space equals a discrete curl of the smearings times structure times momentum density. HKT/gap-5 rigidity workers cite it when wiring the kinetic-normalized weak target. Proof is a short transport: invoke the local-profile ham-ham identity, then rewrite densities and coefficients.
Claim. Let $N,M:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and let $x$ be a point of the two-site phase space. Write $H^{\mathrm{vac}}_j(x)$ for the vacuum-kinetic Hamiltonian density at site $j$, built from the local profile $A(a)p^2+W(a,b)$. Then $\{\sum_j N_j H^{\mathrm{vac}}_j,\,\sum_j M_j H^{\mathrm{vac}}_j\}(x)=\sum_j(N_j M_{j+1}-M_j N_{j+1})\,S_j(x)\,\pi_j(x)$, where $S_j$ and $\pi_j$ are the structure and momentum densities.
background
Module setting is Wave C4/C5 gap 5: mod-vacuum kill plus kinetic-normalized rigidity. The vacuum-kinetic local profile is $h(a,b,p)=A(a)p^2+W(a,b)$; the site density is that profile evaluated on neighboring configuration coordinates and the local momentum. Smeared Hamiltonians are linear combinations $\sum_j N_j h(\ldots)$ over $\mathbb{Z}/2\mathbb{Z}$.
Upstream, LocalHamFromProfile packages exactly those smearings, and the vacuum-kinetic density is definitionally equal to that packaging. A coefficient identity equates the local $h_b h_p$ product for this profile to structure times momentum density. Smoothness of the vacuum-kinetic profile is recorded so the general local ham-ham calculus applies.
The ambient bracket is the phase-space Poisson bracket on the two-site system; the target algebraic shape is the standard HKT point-split ham-ham form with structure and momentum densities on the right-hand side.
proof idea
Apply the general local-profile identity local_profile_ham_ham_form to the vacuum-kinetic profile and its smoothness witness, at smearings $N,M$ and point $x$. That yields the ham-ham expansion in local coefficient form.
Then simpa transports names: rewrite the smeared densities via vacuumKineticHam_eq_LocalHamFromProfile, expand the local ham-ham coefficient, and replace the coefficient product by structure times momentum using vacuumKinetic_localCoeff_eq_structure_mom. No further calculus; pure identification of terms.
why it matters
Feeds vacuumKineticWeakTarget, the HKT point-split dynamical target whose Hamiltonian density is the vacuum-kinetic one and whose structure/momentum fields are the dynamical pair. That target is the kinetic-normalized half of the gap-5 ledger: after mod-vacuum kill, rigidity is recovered under the kinetic-normalized canonical-momentum intensivity field, with FTC recovery theorem-derived rather than assumed.
In the SevenGaps gravity stack this closes the algebraic ham-ham slot for the vacuum-kinetic inhabitant, so the weak target can be assembled without an extra hypothesis. It sits inside the C5 upgrade path (D-gap5-acceptance-adjudication) that flips gap5_constraint_recovery once both ledger halves bind green. Not a T0-T8 forcing step; it is continuum HKT structure needed for the gravity-side rigidity verdict.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.