vacuumKineticHamAdvFrom
plain-language theorem explainer
Defines the site-local “advance-from” Hamiltonian flux for the vacuum-kinetic model on the two-site lattice: minus the Poisson bracket of the Kronecker-localized momentum density against the Kronecker-localized vacuum-kinetic Hamiltonian density. Cited when assembling the weak HKT point-split target and when proving the momentum–Hamiltonian split identity. Body is a direct one-line packaging of the model Poisson bracket.
Claim. On the two-site phase space $(q,\pi)\in(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})^2$, the vacuum-kinetic advance-from density at site $j$ is $-\{F_j,G_j\}(q,\pi)$, where $F_j=\sum_i\delta_{ji}\,\pi_{i+1}(q_{i+1}-q_i)$ is the Kronecker-localized dynamical momentum density and $G_j=\sum_i\delta_{ji}\,H^{\mathrm{vac}}_i$ is the Kronecker-localized vacuum-kinetic Hamiltonian density built from the local profile in $(q_i,q_{i+1},\pi_i)$.
background
The ambient setting is the Wave C4/C5 gap-5 terminal: mod-vacuum kill plus kinetic-normalized rigidity on the two-site periodic lattice. Phase space is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. Observables are real functionals of that pair; their Poisson bracket is the standard sum over sites of $\partial_q F,\partial_\pi G-\partial_\pi F,\partial_q G$, with the usual caveat that nondifferentiable points inject the junk value $0$ from fderiv.
The Kronecker weight $\mathrm{siteDelta},j$ collapses lattice sums to a single site. Dynamical momentum density at site $j$ is $\pi_{j+1}(q_{j+1}-q_j)$. Vacuum-kinetic Hamiltonian density evaluates the local profile $A(q_j)\pi_j^2+W(q_j,q_{j+1})$ at that site. The advance-from scalar packages the signed bracket of those two localized densities, matching the structure-function slot expected by the HKT point-split target interface.
proof idea
Definitional packaging, not a proof. The body is the model Poisson bracket applied to two functionals: the first is the site-$j$ Kronecker collapse of dynamical momentum density, the second the same collapse of vacuum-kinetic Hamiltonian density, evaluated at the given phase-space point and prefixed by a minus sign. No lemmas are invoked; downstream theorems unfold this abbreviation and compute the bracket under ContDiff/DifferentiableAt hypotheses already established for the vacuum-kinetic profile.
why it matters
Fills the hamAdvFrom field of the vacuum-kinetic weak point-split target, so the vacuum-kinetic Hamiltonian density can sit inside the HKT dynamical point-split interface on two sites. That target is the kinetic-normalized side of gap 5: after the mod-vacuum kill rules out the rigid mod-vacuum statement, the remaining work is to show the normalized canonical-momentum structure still recovers the expected constraint algebra. The companion split theorem mom_ham_split_vacuumKinetic expands ${M(w),\sum N_j H^{\mathrm{vac}}_j}$ into weighted combinations of advance-from and advance-to densities; this definition supplies the advance-from half. In the Recognition gravity ledger it is scaffolding for the C5 upgrade binding (D-gap5-acceptance-adjudication), not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.