quarticBalancedHamAdvFrom2
plain-language theorem explainer
The source advection density for the balanced quartic Hamiltonian on the two-site lattice is identically zero. HKT/gravity workers cite it when wiring the weak point-split target or expanding Poisson brackets of balanced momentum against the quartic Ham. The body is the constant-zero functional: source support of ∂_q Mom_j sits only at the neighbor site j+1, so the same-site {Mom δ_j, Ham δ_j} advection vanishes.
Claim. For every phase-space point $x$ on the $2$-site lattice and every site $j\in\mathbb{Z}/2\mathbb{Z}$, the honest source advection density of the balanced quartic Hamiltonian (the contribution of $\{M_j,H_j\}$) equals $0$.
background
Module setting is Wave C2 gap5: inhabit a repaired CanonicalMom / weak point-split target on $n=2$ and separate the balanced quartic from strong rigidity (binding design D-qg-hkt-rigidity-route-20260722). No ledger flag is flipped.
Phase space is the canonical lattice field $(q,\pi):(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})^2$. The model smeared Hamiltonian is $H[N]=\sum_i N_i(\pi_i^2+(q_{i+1}-q_i)^2)/2$. Point-split dynamics packages Ham/Mom densities plus structure and advection maps; the advection pair records the two directed contributions inside ${M_j,H_k}$.
Here the balanced quartic is the falsifying density used to kill strong rigidity while still inhabiting the weak schema. Source advection is the same-site channel ${M_j,H_j}$; target advection is the neighbor channel ${M_j,H_{j+1}}$.
proof idea
Definitional constant: the body is the real number $0$ for every phase-space argument and every $j\in\mathbb{Z}/2\mathbb{Z}$. No lemmas are applied. The doc-comment supplies the geometric reason (support of $\partial_q M_j$ only at site $j+1$), but the Lean object itself is just the zero map used as the hamAdvFrom field of the weak target.
why it matters
Fills the source-advection slot of the balanced-quartic weak point-split inhabitant. Downstream, quarticBalancedWeakTarget sets hamAdvFrom := quarticBalancedHamAdvFrom2, so the weak schema on $n=2$ is inhabited by an explicit density package. The Poisson identity bracket_MomBalanced_quarticHam expands ${M^{\mathrm{bal}}[w],H^{\mathrm{quartic}}[N]}$ as a weighted sum of target-minus-source advection; the source term is this zero map, leaving only the neighbor contribution.
In the gap5 program this is Session B bookkeeping: exhibit an honest HamDyn-style package, separate the balanced quartic from strong rigidity, and bank the DEFINED-only CanonicalMom rigidity statement for later sessions. It is local gravity scaffolding, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.