computedHamAdvTo
plain-language theorem explainer
Defines the target advection density as the Poisson bracket of momentum smeared by a Kronecker weight at site j against Hamiltonian density smeared at site j+1. Gravity workers cite it when tying free advection slots in the point-split HKT schema to the Mom–Ham bracket calculus. The body is a direct two-argument application of the model bracket to those smeared densities.
Claim. For a point-split HKT dynamical target $T$ on an $n$-site lattice ($n\ge 1$), phase-space point $x$, and site $j\in\mathbb{Z}/n\mathbb{Z}$, the computed target advection is $\{M[\delta_j],\,H[\delta_{j+1}]\}(x)$, where $M[\delta_j]=\sum_i \delta_{j,i}\,m_i$ is the momentum density smeared by the Kronecker weight at $j$ and $H[\delta_{j+1}]$ is the Hamiltonian density smeared at $j+1$.
background
The module repairs the weak point-split HKT target after an adversarial pass showed HKTPointSplitTargetDyn is decoy-inhabitable by quartic zero-momentum data. The strong class forces advection slots to equal Mom–Ham bracket extractions rather than free decorative fields.
Phase space is the lattice pair $(q,\pi)$ on $\mathbb{Z}/n\mathbb{Z}$. 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 junk zero when derivatives fail. The Kronecker weight siteDelta k is $1$ at site $k$ and $0$ elsewhere, so smearing collapses to a single-site density.
Upstream, the weak schema already records source/target advection densities in the identity ${D[w],H[N]}=\sum_j w_j(N_{j+1}\cdot\mathrm{hamAdvTo}_j-N_j\cdot\mathrm{hamAdvFrom}_j)$. This definition supplies the bracket-calculus value that the strong class demands those target slots equal.
proof idea
Pure definition: evaluate the model Poisson bracket at $x$ on the two smeared observables $y\mapsto\sum_i\delta_{j,i},m_i(y)$ and $y\mapsto\sum_i\delta_{j+1,i},h_i(y)$. No lemmas or tactics; the body is the term that instantiates bracket on those two functionals.
why it matters
Closes the gap between free advection fields in the weak schema and the hypersurface-deformation calculus. Downstream, hamAdvTo_eq_computed proves that under mom_ham_split at $n=2$ the target's own hamAdvTo equals this computed value. The strong structure HKTPointSplitTargetDynStrong then requires that equality as a field, together with load-bearing momentum and kinetic regularity, so quartic zero-momentum decoys are excluded.
In the SevenGaps gravity program this is part of Wave C2: honest HKT inhabitants must have advection tied to ${M,H}$, not arbitrary slots. Strong-class rigidity itself is already falsified (balanced quartic); binding rigidity moves to CanonicalMom. This definition remains the extraction map that makes the advection-tie checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.