computedHamAdvFrom
plain-language theorem explainer
Defines source advection density as the negative Poisson bracket of the Kronecker-smeared momentum and Hamiltonian densities at the same site j. Gravity workers cite it when tying free advection slots in the weak HKT point-split schema to the Mom–Ham calculus. The body is a direct one-line evaluation of the model bracket on those two smeared observables.
Claim. For a point-split HKT target $T$ on $n$ sites ($n\ge 1$), phase-space point $x$, and site $j\in\mathbb{Z}/n\mathbb{Z}$, the computed source advection is $-\{\mathrm{Mom}[\delta_j],\,\mathrm{Ham}[\delta_j]\}(x)$, where $\delta_j$ is the Kronecker weight at $j$ and the smeared densities are $\sum_i \delta_j(i)\,T.\mathrm{momDensity}(y,i)$ and $\sum_i \delta_j(i)\,T.\mathrm{hamDensity}(y,i)$.
background
This module repairs the weak point-split HKT target after an adversarial pass showed the weak schema is decoy-inhabitable by quartic zero-momentum data. The local setting is hypersurface-deformation calculus on a cyclic lattice of $n$ sites: phase space carries configuration and momentum fields, and observables are real functions of that phase space.
The model Poisson bracket is ${F,G}(x)=\sum_i(\partial_{q_i}F,\partial_{p_i}G-\partial_{p_i}F,\partial_{q_i}G)$, with the usual caveat that nondifferentiable points feed the junk value $0$ from fderiv. Smeared momentum and Hamiltonian densities come from the weak structure HKTPointSplitTargetDyn, whose source advection field is intended to appear in ${D[w],H[N]}=\sum_j w_j(N_{j+1}\cdot\mathrm{hamAdvTo}_j-N_j\cdot\mathrm{hamAdvFrom}_j)$. The weight siteDelta j is the Kronecker lapse/shift on $\mathbb{Z}/n\mathbb{Z}$.
proof idea
Definition, not a proof. It packages one evaluation of the model bracket: smear momDensity and hamDensity by the same Kronecker weight at site $j$, form $-{\mathrm{Mom},\delta_j,,\mathrm{Ham},\delta_j}$ at $x$, and return that real. No lemmas are applied; downstream equalities unfold this def and invoke mom_ham_split.
why it matters
In the strong target, advection slots are no longer free decorative fields: they must equal these bracket-calculus extractions. Downstream, hamAdvFrom_eq_computed proves that under mom_ham_split at $n=2$, the schema's source slot equals this value; the twin hamAdvTo_eq_computed does the same for the target slot. The strengthened structure HKTPointSplitTargetDynStrong records both equalities as fields, together with load-bearing momentum and kinetic regularity, so that the quartic zero-momentum decoy is excluded while an honest inhabitant still passes.
This is Wave C2 repair infrastructure in the SevenGaps gravity stack, not a T0–T8 forcing step. Binding rigidity has already moved to the CanonicalMom line; the present def only pins what "advection tied to Mom–Ham bracket calculus" means concretely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.