MomBalancedD
plain-language theorem explainer
Explicit Fréchet derivative (as a continuous linear map) of the weight-averaged balanced momentum density on the two-site lattice phase space. HKT rigidity and CanonicalMom workers cite it when extracting configuration and momentum partials of the balanced quartic. The body is the product-rule map f(x)·Dg + g(x)·Df with f = π₀+π₁ and g the quadratic structure factor in the q-coordinates.
Claim. For weights $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and a point $x=(q,\pi)$ in the two-site phase space $(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$, the continuous linear map $DM_w(x):T_x\to\mathbb{R}$ is the product-rule derivative of $M_w=(\pi_0+\pi_1)\,g_w(q)$ with $g_w(q)=w_0(1+q_1^2)+w_1(1+q_0^2)$, written via the coordinate functionals for $q_i$ and $\pi_i$.
background
The ambient module is Wave C2 gap5: kill strong rigidity and repair the CanonicalMom class along the D-qg-hkt-rigidity route. Session B defines the CanonicalMom point-split target, exhibits an honest HamDyn inhabitant, and separates the balanced quartic; no ledger flag is flipped.
Phase space on $n$ sites is the product of configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. The maps $\mathrm{coord}q(i)$ and $\mathrm{coord}\pi(i)$ are the continuous linear functionals extracting $q_i$ and $\pi_i$.
The scalar field being differentiated is the weight-averaged balanced momentum density $M_w(x)=\sum_j w_j,\mu_j(x)$ on $n=2$, which factors as $(\pi_0+\pi_1)$ times a quadratic structure factor in the $q$-coordinates.
proof idea
Pure definition: no tactic proof. The body writes the product-rule Fréchet data $f(x)\cdot Dg+g(x)\cdot Df$ with $f=\pi_0+\pi_1$ and $g_w(q)=w_0(1+q_1^2)+w_1(1+q_0^2)$. Linear pieces come from $\mathrm{coord}\pi(0)+\mathrm{coord}\pi(1)$ and from $2q_j,\mathrm{coord}_q(j)$ scaled by the weights; scalar multiplications by the field values at $x$ assemble a single map $\mathrm{PhaseSpace}_2\to L[\mathbb{R}],\mathbb{R}$.
why it matters
Feeds the lemma that $M_w$ is Fréchet differentiable with this derivative, and the two theorems that evaluate the configuration and momentum partials by applying the map and simplifying. Those partials are the computational spine of Session B: separate the balanced quartic from the honest HamDyn inhabitant and bank the DEFINED-only CanonicalMom rigidity statement for $n=2$. Local to the HKT point-split rigidity route (gap5); it does not touch the T0–T8 forcing chain, RCL, or the alpha band, and it leaves $\mathtt{gap5_constraint_recovery}$ false.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.