quarticBalancedHamAdvTo2
plain-language theorem explainer
Defines the honest “to” advection density for the balanced quartic Hamiltonian on two-slot phase space: 8(π₀+π₁) q_{j+1} π_{j+1}³. Gravity/HKT authors cite it when assembling Poisson brackets of balanced momentum against the quartic Ham. It is a pure closed-form density, not a proved identity.
Claim. On two-component phase space with coordinates $(q_0,q_1)$ and momenta $(\pi_0,\pi_1)$, the honest target advection density from $\{M\delta_j, H\delta_{j+1}\}$ is $8(\pi_0+\pi_1)\, q_{j+1}\, \pi_{j+1}^3$, for each slot $j\in\mathbb{Z}/2\mathbb{Z}$.
background
Module setting is Wave C2 gap5: kill strong point-split rigidity and repair the CanonicalMom class (binding design D-qg-hkt-rigidity-route-20260722). Session B exhibits an honest HamDyn inhabitant for the balanced quartic and banks a DEFINED-only CanonicalMom rigidity statement; no ledger flag is flipped.
Phase space here is the two-slot discrete field $(q_j,\pi_j)_{j\in\mathbb{Z}/2}$. The balanced quartic Hamiltonian density is the quartic momentum form used as a falsifier of strong rigidity and as a weak point-split target. Advection densities package the local contributions that appear when one expands Poisson brackets ${M,H}$ slot-by-slot.
The companion “from” density handles ${M\delta_j, H\delta_j}$-type terms; this definition is the crossed “to” piece ${M\delta_j, H\delta_{j+1}}$. The factor $8(\pi_0+\pi_1)$ is the balanced total-momentum weight that makes the later Wronskian identity $(m_0-m_1)=2(\pi_0+\pi_1)(q_1 S_0-q_0 S_1)$ hold cleanly.
proof idea
Definitional abbreviation only: the body is the closed-form real expression $8\cdot(x.2,0+x.2,1)\cdot x.1(j+1)\cdot(x.2(j+1))^3$. No tactics, no lemmas, no reduction. Downstream proofs treat it as a named density and expand brackets by substituting this formula.
why it matters
Feeds the Poisson-bracket identity bracket_MomBalanced_quarticHam, which expands ${M^{\mathrm{bal}},H^{\mathrm{quartic}}}$ as a weighted sum of “from” and “to” advection densities. Also plugs directly into quarticBalancedWeakTarget as the hamAdvTo field, so the balanced quartic inhabits the weak point-split dynamical schema on $N=2$.
In the gap5 program this is the honest (non-scaffolded) advection chosen so the balanced quartic separates from strong rigidity while still giving a well-typed CanonicalMom target. It does not flip gap5_constraint_recovery; sessions C still owe the CanonicalMom rigidity proof. Framework-wise it sits in the discrete gravity/HKT ledger layer that interfaces with eight-tick and $D=3$ forcing only indirectly, via the broader SevenGaps stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.