quarticBalancedMomBracketDensity2
plain-language theorem explainer
Wronskian density for the balanced-momentum Poisson bracket on the two-site lattice. It packages the factor $(\pi_0+\pi_1)(q_{j+1}S_j-q_j S_{j+1})$ that appears when the balanced-momentum bracket expands. Anyone proving nonabelian $\{M,M\}$ for the balanced quartic model cites it. Pure definitional packaging of the algebraic factor chosen so $(m_0-m_1)=2(\pi_0+\pi_1)(q_1 S_0-q_0 S_1)$.
Claim. For a phase-space point $x=(q,\pi)$ on the two-site periodic lattice and site index $j\in\mathbb{Z}/2\mathbb{Z}$, the balanced-momentum bracket density is $(\pi_0+\pi_1)\bigl(q_{j+1}S_j(x)-q_j S_{j+1}(x)\bigr)$, where the structure function is $S_k(x)=1+q_k^2$.
background
The ambient setting is Wave C2 gap5 in the HKT point-split program: kill strong rigidity on $n=2$ and repair a CanonicalMom class, without flipping the ledger flag gap5_constraint_recovery. Phase space is the product of configuration and conjugate momentum on a periodic lattice, here $n=2$: $x=(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$.
The structure function used throughout the balanced quartic model is $S_j(x)=1+q_j^2$, the same shape as the dynamical structure density. Balanced momentum functionals are built from that structure together with a shared kinetic factor involving $\pi_0+\pi_1$. The Poisson bracket ${M_v,M_w}$ of two such momenta is expected to be nonabelian; the density defined here is the local Wronskian factor that carries that noncommutativity.
The doc-comment fixes the normalization: the density is chosen so that the momentum-density difference satisfies $(m_0-m_1)=2(\pi_0+\pi_1)(q_1 S_0-q_0 S_1)$. That identity is the algebraic reason the factor appears in the expanded bracket.
proof idea
Definitional, not a proof. The body multiplies the total momentum sum $\pi_0+\pi_1$ by the discrete Wronskian $q_{j+1}S_j-q_j S_{j+1}$, with $S$ the structure $1+q^2$ at the two neighboring sites. No lemmas are applied; the expression is the packaged right-hand side that later bracket expansions match against.
why it matters
This density is the load-bearing local factor in the balanced-momentum sector of the repaired CanonicalMom route. The parent identity bracket_MomBalanced_MomBalanced expands ${M_v,M_w}$ as a sum over $j$ of the skew coefficient $(v_j w_{j+1}-w_j v_{j+1})$ times this density. From that expansion, quarticBalanced_mom_load_bearing_witness evaluates at a concrete load phase with basis smearings and obtains a nonzero bracket, proving the balanced momenta are genuinely nonabelian.
The same package is wired into quarticBalancedWeakTarget, the weak point-split inhabitant for the balanced quartic. In the module plan this supports Session B: separate the balanced quartic from the honest HamDyn inhabitant and bank the DEFINED-only CanonicalMom rigidity statement for later sessions. It does not itself close gap5; it supplies the concrete nonabelian witness density that the rigidity and target constructions need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.