hamDynAdvFrom
plain-language theorem explainer
Source advection density for the Poisson bracket of dynamic momentum against the dynamic Hamiltonian on the two-site lattice. It is the local factor multiplying the smear weight N_j when that bracket expands as a weighted difference of source and target densities. Downstream point-split HKT inhabitants and vacuum-sector kill lemmas cite it by name. The body is a pure algebraic formula: neighboring-momentum product plus the quadratic nearest-neighbor gradient term weighted by (1+q_j^{2}).
Claim. For a phase-space point $x=(q,\pi)$ on the two-site periodic lattice $\mathbb{Z}/2\mathbb{Z}$ and a site index $j$, the source advection density is $\pi_j\,\pi_{j+1}+(1+q_j^2)\,(q_{j+1}-q_j)^2$.
background
The ambient setting is the Wave C2 R5 repair of the Hojman–Kuchař–Teitelboim (HKT) dynamic target. The unsplit Dyn target keeps a single mom_ham field that is uninhabitable for honest nearest-neighbor momentum profiles against the frozen quadratic Hamiltonian at $n=2$: unsplit advection forces $(p_0+p_1)\cdot\partial_d f=p_0^2+d^2$, singular on $p_0+p_1=0$. This module is the repaired sibling, using smeared point-split source/target advection densities instead of an unsplit field.
Phase space is the product $(q,\pi):(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$. The dynamic Hamiltonian is the smear of the quadratic density $\pi_i^2+(1+q_i^2)(q_{i+1}-q_i)^2$ against a lapse $N$. Dynamic momentum is the smear of a local momentum density against a weight $w$. On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the symmetric deformation generator vanishes identically and the older $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch is empty; the load-bearing structure uses these advection densities instead.
proof idea
Definitional, not a proof. The body writes the two-term local density directly: product of neighboring conjugate momenta $\pi_j\pi_{j+1}$, plus the quadratic nearest-neighbor configuration gradient $(q_{j+1}-q_j)^2$ weighted by the conformal factor $(1+q_j^2)$. No lemmas are applied; the expression is the closed form that later appears as the coefficient of $-N_j$ in the expanded bracket ${M_w,H_N}$.
why it matters
This density is the source half of the honest point-split advection law for dynamic HKT at $n=2$. The bracket identity bracket_MomDyn_HamDyn expands ${M_w,H_N}$ as $\sum_j w_j,(N_{j+1},\mathrm{advTo}_j-N_j,\mathrm{advFrom}_j)$, so the formula here is load-bearing for that expansion. It is installed as the hamAdvFrom field of hamDynPointSplitTarget, the honest HamDyn inhabitant of the repaired point-split Dyn target (the strong class after the unsplit target was left as a falsification-adjacent record).
The vacuum-sector kill module reuses it verbatim as vacuumShiftHamAdvFrom (source advection is unchanged by the vacuum shift, which has vanishing $\pi$-partial) and feeds the analogous bracket against the vacuum Hamiltonian. No rigidity theorem is proved in this module; no ledger flag is flipped. The declaration closes the API gap left when $D_{\mathrm{gen}}^{\mathrm{sym}}$ became definitionally empty at HamDyn size on $\mathbb{Z}/2\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.