MomBalanced
plain-language theorem explainer
Defines the smeared balanced-quartic momentum on the two-site lattice phase space: a weight function times the load-bearing momentum densities, summed over Z/2Z. Gravity and HKT-rigidity workers cite it as the CanonicalMom observable for the repaired point-split target. The body is a one-line weighted sum of the density model.
Claim. For weights $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and a phase-space point $x=(q,\pi)$ on the two-site lattice, the balanced momentum is $M_w(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\, m_j(x)$, where each density is $m_j(x)=(\pi_0+\pi_1)\cdot s(x,j+1)$ and $s$ is the balanced quartic structure factor.
background
The ambient setting is Wave C2 gap5: kill strong rigidity and repair the CanonicalMom class on the two-site HKT point-split target (binding design D-qg-hkt-rigidity-route). Session B separates an honest HamDyn inhabitant from the balanced quartic and banks a DEFINED-only CanonicalMom rigidity statement; no ledger flag is flipped.
Phase space is the product of configuration and conjugate momentum maps on the periodic lattice: $x=(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$. The load-bearing momentum density is $m_j=(\pi_0+\pi_1)\cdot s(x,j+1)$, chosen so the balance identity $s_0\cdot m_0=s_1\cdot m_1$ cancels the ham-ham right-hand side on $\mathbb{Z}/2\mathbb{Z}$.
The smeared observable packages those densities against an arbitrary weight $w$, matching the usual ADM-style smearing of momentum constraints by lapse/shift-like test functions on the lattice.
proof idea
Definition only: expand as the finite sum over $j\in\mathbb{Z}/2\mathbb{Z}$ of $w(j)$ times the balanced quartic momentum density at site $j$. No lemmas are applied; later closed-form and derivative lemmas unfold this sum and the density definition.
why it matters
This is the momentum half of the repaired CanonicalMom package for gap5 Session B. Downstream it is the left argument of the Poisson brackets bracket_MomBalanced_MomBalanced and bracket_MomBalanced_quarticHam, which encode the deformation algebra against itself and against the balanced quartic Hamiltonian. Differentiability (hasFDerivAt_MomBalanced, differentiable_MomBalanced), the closed two-term form (MomBalanced_closed), and the partials in $p$ and $q$ all hang off this definition, as does the load-bearing witness that the balanced quartic supplies an honest CanonicalMom inhabitant.
In the broader Recognition gravity stack this is lattice bookkeeping for hypersurface deformation, not a T0-T8 forcing step. It supports the route that kills the strong point-split rigidity claim while keeping a well-posed CanonicalMom target for later sessions to prove.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.