vacuumKineticHamAdvTo
plain-language theorem explainer
Defines the directed Poisson advection of vacuum kinetic Hamiltonian density from site j+1 onto the momentum density at site j, on the two-site periodic phase space. Gravity/HKT authors cite it as the hamAdvTo structure field of the vacuum-kinetic weak target. It is a pure definition: the Poisson bracket of the Kronecker-localized momentum density against the Kronecker-localized vacuum kinetic Hamiltonian density.
Claim. For a phase-space point $x=(q,\pi)$ on the two-site lattice and a site index $j\in\mathbb{Z}/2\mathbb{Z}$, the vacuum-kinetic Hamiltonian advection-to density is the Poisson bracket $\{M_j, H_{j+1}\}(x)$, where $M_j$ is the momentum dynamical density supported only at site $j$ and $H_{j+1}$ is the vacuum kinetic Hamiltonian density supported only at site $j+1$.
background
The ambient setting is the two-site periodic lattice wave field of hypersurface deformation theory. Phase space is pairs $(q,\pi)$ of configuration and conjugate momentum maps $\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. The model Poisson bracket is ${F,G}(x)=\sum_i(\partial_{q_i}F,\partial_{\pi_i}G-\partial_{\pi_i}F,\partial_{q_i}G)$, with the usual caveat that nondifferentiable observables contribute the junk value $0$.
siteDelta is the Kronecker weight that localizes a density to a single lattice site. Momentum dynamical density at site $j$ is $\pi_{j+1}(q_{j+1}-q_j)$. Vacuum kinetic Hamiltonian density is the local profile of the vacuum-kinetic model evaluated on $(q_j,q_{j+1},\pi_j)$.
The module closes Wave C4/C5 gap5: mod-vacuum kill plus kinetic-normalized rigidity. This definition supplies one directed advection leg of the vacuum-kinetic point-split target.
proof idea
Definition only: no proof obligations. The body is the model Poisson bracket applied to two localized observables. The first argument sums Kronecker weights at $j$ times momentum dynamical density; the second sums Kronecker weights at $j+1$ times vacuum kinetic Hamiltonian density; both are evaluated at the given phase-space point $x$.
why it matters
Feeds the vacuum-kinetic weak target package, where it is installed as the hamAdvTo field of the dynamical point-split target on two sites. That target is the structure object against which kinetic-normalized rigidity and the momentum-Hamiltonian split are checked.
Downstream, mom_ham_split_vacuumKinetic expands the global bracket of total momentum against the $N$-weighted vacuum kinetic Hamiltonian into a sum of terms built from this advection density (and its companion advection-from). In the gap5 ledger this is the vacuum-kinetic half of the C5 upgrade: after both ledger halves bind green, constraint recovery flips under Gap5ConstraintCloseStatus.
No T0-T8 forcing step is claimed here; the declaration is local HKT bookkeeping on $n=2$, not a derivation of $D=3$ or $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.