Theorem. A convergent expansion over closed walks [fdip-0071]
AGENTDRAFTED
Let the vertices be
\(\Lambda =\prod _{j=1}^d\mathbb Z/L_j\mathbb Z\), with \(L_j\ge 3\).
Give each edge \((x,j):x\to x+e_j\) weight one and a unitary or
orthogonal transport \(U_{x,j}\) on a fixed fiber. For the
determinant action, put \(D=2d+m^2\), where \(m>0\),
and let \(H_U\) be the covariant adjacency operator. Then
\[Q_U=DI-H_U,\qquad \|H_U\|\le 2d<D,\]
and
\[W(U)=\kappa N\log D-
\kappa \sum _{k\ge 1}\frac {\operatorname {tr}_{\mathbb K}(H_U^k)}{kD^k}.\]
The series is absolutely convergent, uniformly over all such unitary
connections. For \(K\ge 0\), its remainder after length \(K\) satisfies
\[|R_K(U)|\le \frac {\kappa N}{K+1}
\frac {(2d/D)^{K+1}}{1-2d/D}.\]
Each trace is the sum of fiber holonomy traces over all based oriented
closed nearest-neighbor walks of length \(k\).
Mathlib's
Real.hasSum_pow_div_log_of_abs_lt_one states, for a real
\(x\) with \(|x|<1\),
\[\sum _{n\ge 0}\frac {x^{n+1}}{n+1}=-\log (1-x).\]
It supplies the scalar series used for each real eigenvalue. Spectral
reduction, the walk interpretation, the lattice norm bound and the
uniform trace remainder are the additional arguments above; the
formal declaration does not state this lattice expansion.
The numerical bound \(2d\) and scalar diagonal \(D\) use this
regular lattice and its unit edge weights. For arbitrary weights or
degrees one must change the diagonal decomposition and norm estimate;
the displayed bound is not asserted unchanged.
Kazakov and Migdal integrate an adjoint matrix field in a different
lattice model. Their Section 2, equations (3)–(4), gives a trace-log
and loop weights involving \(|\operatorname {tr}U[\Gamma ]|^2\)
[kazakov1992induced, p. 2]. This is a comparison with the
closed-walk method. The finite real-scalar coefficient below follows
from the present proof, not from their large-\(N\) analysis or a
continuum identification.