hamAdvectionSplit
plain-language theorem explainer
Packs source and target Hamiltonian advection densities of a point-split HKT dynamic target into one shift-keyed real slot. Gravity workers repairing the n=2 HKT momentum–Hamiltonian sector cite it as DgenSym-shaped packaging. The body is a one-line conditional: average of the two densities when the shift is 1, else zero. At n=2 the packaging is documentary only, since the generator symmetry vanishes.
Claim. Given a point-split HKT dynamic target $T$ on $n$ lattice sites, a phase-space point $x$, and indices $a,j\in\mathbb{Z}/n\mathbb{Z}$, return $\tfrac12\bigl(h^{\mathrm{to}}_j(x)+h^{\mathrm{from}}_j(x)\bigr)$ if $a=1$, and $0$ otherwise, where $h^{\mathrm{to}}$ and $h^{\mathrm{from}}$ are $T$'s target and source advection densities in the smeared bracket $\{D[w],H[N]\}$.
background
The ambient setting is the Wave C2 R5 repair of the Hojman–Kuchař–Teitelboim dynamic target. The unsplit momentum–Hamiltonian field is uninhabitable for honest nearest-neighbor local momentum against the frozen quadratic Hamiltonian: at $n=2$ it forces a singular identity on $p_0+p_1=0$. This module is the repaired sibling; the load-bearing class is the strong point-split target, while the weak structure used here is schema-only.
Phase space is the product of configuration and conjugate momentum on the periodic lattice $\mathbb{Z}/n\mathbb{Z}$. The dynamic Hamiltonian density (unfolded for Fréchet calculus) is the quadratic form HamDyn summing $N_i/2$ times kinetic plus gradient-squared terms. The point-split target records separate source and target advection densities so that ${D[w],H[N]}=\sum_j w_j(N_{j+1}\cdot h^{\mathrm{to}}_j-N_j\cdot h^{\mathrm{from}}_j)$.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the generator-symmetry functional vanishes identically and any DgenSym-shaped mom_ham_split sketch is definitionally empty. The present packaging therefore only documents the average of the two advection slots under a shift key $a$.
proof idea
Pure definition, not a proof. The body is a single conditional on the shift index $a\in\mathbb{Z}/n\mathbb{Z}$: if $a=1$, return the arithmetic mean of the target's hamAdvTo and hamAdvFrom densities at site $j$; otherwise return $0$. No lemmas are applied.
why it matters
Sits in the Gravity SevenGaps repair path that replaces the unsplit Dyn HKT target after the adjudication that unsplit advection cannot host smooth nearest-neighbor momentum against the frozen quadratic Hamiltonian. It preserves a DgenSym-shaped API surface for source/target advection while remaining honest that, at $n=2$, that symmetry is identically zero.
No downstream theorem currently depends on it (used_by is empty). The module itself proves no rigidity result and flips no ledger flag; the momentum sector is recorded as non-abelian (Wronskian density in mom_mom). The open Prop on the unsplit campaign Hamiltonian remains the falsification-adjacent record. Framework landmarks T0–T8, RCL, and the mass ladder are not touched here; this is local classical-bracket scaffolding inside the lattice gravity campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.