MomBalanced_closed
plain-language theorem explainer
On the two-site phase space, the weighted balanced momentum functional factors as total momentum times a weighted structure sum: $M_w(x)=(\pi_0+\pi_1)\,(w_0 S(x,1)+w_1 S(x,0))$. Anyone differentiating the canonical-momentum target or applying the product rule to Frechet data cites this identity. The proof unfolds the density definition, collapses the $\mathbb{Z}/2$ sum, and finishes by ring.
Claim. For weights $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,\pi)\in T^*\mathbb{R}^{2}$, the weighted balanced momentum $M_w(x):=\sum_{j\in\mathbb{Z}/2} w_j\,m_j(x)$ equals $(\pi_0+\pi_1)\bigl(w_0\,S(x,1)+w_1\,S(x,0)\)$, where each site momentum density is $m_j(x)=(\pi_0+\pi_1)\,S(x,j+1)$ and $S$ is the balanced quartic structure density.
background
Module setting is Wave C2 gap5 on the HKT point-split route: Session B repairs the CanonicalMom class after the strong rigidity statement is killed by the balanced quartic falsifier. No ledger flag flips; gap5_constraint_recovery stays false.
Phase space is the two-site cotangent bundle. The load-bearing momentum density is $m_j=(\pi_0+\pi_1)\cdot S(x,j+1)$, chosen so the balance identity $S_0 m_0=S_1 m_1$ cancels the ham-ham right-hand side on $\mathbb{Z}/2$. The weighted functional is the finite sum $M_w=\sum_j w_j m_j$.
Upstream arithmetic is elementary: sum_zmod2 expands $\sum_{j:\mathbb{Z}/2} g(j)=g(0)+g(1)$, and the wrap lemmas $(0+1=1)$, $(1+1=0)$ identify the shifted structure indices.
proof idea
Term-mode proof. Unfold $M_w$ and the density $m_j=(\pi_0+\pi_1)S(x,j+1)$. Simplify with sum_zmod2 to a two-term sum, then apply the $\mathbb{Z}/2$ addition facts so the structure arguments become $1$ and $0$ respectively. Factor $(\pi_0+\pi_1)$ and finish by ring. No analytic or dynamical lemmas are needed.
why it matters
Parent consumer is hasFDerivAt_MomBalanced, whose doc frames the result as product-rule Frechet data $f,g'+g,f'$ with $f=\pi_0+\pi_1$. Closing the closed-form identity is the algebraic prerequisite for that derivative lemma, which in turn supports the honest HamDyn inhabitant of HKTPointSplitTargetDynCanonicalMom.
In the gap5 program this separates the balanced quartic from the canonical-momentum target and banks the DEFINED-only rigidity statement for later sessions. It is local gravity scaffolding on the two-site register, not a T0-T8 forcing step, but it keeps the repaired CanonicalMom class mathematically usable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.