The formal residue is the coefficient of after coefficients have been moved to the left by the formal pseudodifferential composition rule. It is not an analytic residue at a point. For scalar coefficients, the residue of a commutator is a total derivative; integrating it with vanishing boundary terms produces the cyclic Adler trace.
For a fixed formal pseudodifferential operator and a monic differential operator , cyclicity of the Adler trace gives with and . The function is affine in the variable coefficients; its variational derivative with respect to is .
A field has infinitely many degrees of freedom: its initial state is a function rather than a finite list of coordinates. For a Hamiltonian evolution, the analogue of the finite-dimensional construction seeks an infinite sequence of independent conserved functionals whose Poisson brackets vanish. Their Hamiltonian vector fields then define commuting time evolutions. For example, a Poisson operator produces the field equation , where is the variational derivative.
A Lax equation packages many conservation laws into one operator identity. If , cyclicity of an appropriate trace gives
For a formal pseudodifferential operator the relevant trace is the Adler trace; suitable fractional powers of a monic differential operator produce further conserved functionals. A Lenard-Magri recursion can prove that such functionals are Poisson-commuting functions, rather than merely conserved quantities. A Lax equation by itself does not establish all the independence and completeness properties needed for integrability.
The Korteweg-De Vries equation illustrates the mechanism. In one time normalization take and . Direct composition gives
Its spectral problem, together with the inverse scattering transform for decaying data or suitable spectral coordinates for periodic data, turns nonlinear evolution into simple evolution of spectral data. Solitary waves arise from discrete spectral data, while continuous data describe dispersive radiation.
Thus infinite-dimensional Hamiltonian integrability is more than an infinite list of formulas: one wants sufficiently complete commuting invariants and a reconstruction mechanism that solves the evolution. Boundary conditions and the function space are essential. A formal hierarchy need not converge, and an infinite family of conserved quantities does not automatically give a compact infinite-dimensional torus or an unrestricted analogue of the Arnold-Liouville theorem.
Write , setting unused coefficients to zero. Split the Adler trace into its fixed leading part and variable parts:
Cyclicity from part (i) gives
Thus this Hamiltonian trace functional on monic differential operators has the required form
To make each coefficient explicit, expand by the Leibniz rule. A term with derivatives of contributes to the residue exactly when . Consequently,
These are smooth functions depending on , not on the variable coefficients of . In particular and . The coefficient must be included: it appears in the displayed sum even though the printed coefficient list starts at .
The monic operators form an affine space, not a vector space. Accordingly is affine in the coordinates , with constant , and its differential is linear in variations. Its variational derivatives are . It is the restriction of a linear trace pairing on the full operator space, which explains the terminology without discarding the constant term.
Put every formal pseudodifferential operator in normal order, with all coefficient functions on the left. Its formal pseudodifferential residue is the coefficient of . The Adler trace is
Here and below, use periodic coefficients and integrate over a period, or impose convergence and vanishing boundary terms on the real line. Equivalently, the algebraic integration functional must annihilate total derivatives. This convention is needed for the requested trace property; arbitrary elements of do not supply it automatically.
It suffices to compute with monomials , . Write . If , no term in either product has power , so both residues are zero. If , the formal pseudodifferential composition rule gives
Since , reversal of the factors in the numerator proves
After integrations by parts, . Hence the two product traces agree. More explicitly, for their residue difference is the total derivative
For the residue difference is . In products of operators bounded above in order, only finitely many monomial pairs can contribute to a residue: the required is nonnegative, so the two downward coefficient indices have a bounded sum. Summing the monomial result therefore proves
The boundary convention is substantive. Without it, take , . Both individual residues vanish, but and its integral over is , not zero. The primitive has unequal limits at the two ends. Also a generic smooth residue need not have a convergent integral at all. Thus the proof supplies the intended cyclic trace under its necessary analytic or formal integration convention.