hamDynAdvTo
plain-language theorem explainer
Explicit target advection density for the Poisson bracket of smeared dynamic momentum against the dynamic Hamiltonian on the two-site lattice. Gravity and HKT-structure workers cite it when building the point-split Dyn target or evaluating {Mom, Ham}. The body is a closed cubic polynomial in nearest-neighbor configuration jumps and the target-site momentum; no proof obligations.
Claim. On the two-site phase space $(q,\pi)\in(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})^2$ and site $j\in\mathbb{Z}/2\mathbb{Z}$, the target advection density is $\pi_{j+1}^{2}-(1+q_{j+1}^{2})(q_{j+1}-q_{j})^{2}-q_{j+1}(q_{j+1}-q_{j})^{3}$.
background
The ambient phase space is the product of configuration and conjugate momentum on the periodic lattice: pairs $(q,\pi)$ with both maps $\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, so indices live in $\mathbb{Z}/2\mathbb{Z}$ and $j+1$ is the unique neighbor of $j$.
This module repairs the unsplit dynamic HKT target. The unsplit mom-ham field is uninhabitable for honest nearest-neighbor local momentum against a frozen quadratic Hamiltonian (singular when $p_0+p_1=0$). The repaired API uses smeared point-split momentum with separate source and target advection densities, matching the pattern already used for Hamiltonian-Hamiltonian brackets.
The companion source density and the smeared momentum functional sit alongside this definition; together they feed the Poisson bracket identity that replaces the empty $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch (vacuous at $n=2$ because $-1=1$).
proof idea
Pure definition: no tactics, no lemmas. The right-hand side is written directly as a cubic polynomial in the target-site momentum $\pi_{j+1}$ and the nearest-neighbor jump $\Delta q_j:=q_{j+1}-q_j$, with coefficients built from $q_{j+1}$. Downstream bracket theorems expand partial derivatives of the smeared momentum and Hamiltonian and match coefficients against this expression.
why it matters
Load-bearing density in the repaired point-split Dyn target. It is the hamAdvTo field of the honest HamDyn inhabitant of that target, and it appears verbatim in the identity
$${M_w,H_N}=\sum_j w_j\bigl(N_{j+1},\mathrm{advTo}_j-N_j,\mathrm{advFrom}j\bigr).$$
The vacuum-sector kill module reuses it as the HamDyn slot inside a shifted target advection (subtracting $2\Delta q_j,q{j+1}$), so the same polynomial anchors both the dynamic and vacuum bracket calculations. No rigidity theorem is claimed here; the module only supplies the repaired densities after the unsplit target was adjudicated uninhabitable. Framework context is the SevenGaps HKT campaign on lattice hypersurface deformation, not the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.