The following describes the scope of the Lean formalization related to the following accompanying paper(s):
Scope
Kaplansky's direct-finiteness conjecture asserts that \(ab=1\) implies \(ba=1\) for \(a,b\in K[G]\), for every field \(K\) and group \(G\). The formalized results construct a finite field of characteristic two and a group algebra violating this implication. One statement records the counterexample for a finitely generated group; the more detailed construction gives a finitely presented group with an element of odd prime order.
The detailed construction also gives a precise recipe for choosing the data and proves that the required search terminates. The further conclusion that the group is nonsofic is outside these statements.
A nonsingular integer matrix has absolute determinant at least \(1\). The group-ring Determinant Conjecture extends this bound to matrices over \(\mathbb Z[G]\) for every discrete group \(G\). If \(T_A\) is the operator induced by such a matrix \(A\) on finite direct sums of \(\ell^2(G)\), and \(\mu_A\) is the spectral measure of \(T_A^*T_A\) with respect to the group trace, the conjecture asserts
\(\displaystyle \int_{(0,\infty)}\log t\,d\mu_A(t)\ge0,\)
with the zero spectral atom omitted. For an invertible square matrix, this is equivalent to its Fuglede–Kadison determinant being at least \(1\).
The formalized result contradicts that bound. It gives a finitely generated group \(G\) and an \(n\times n\) matrix over \(\mathbb Z[G]\), with \(n\ge1\), that is invertible over \(\mathbb Q[G]\). Its bounded left-regular operator is invertible and has determinant strictly between \(0\) and \(1\).
The formalization uses the trace of \(\log(T^*T)\) to define the determinant for the invertible operator \(T\). The paper's additional spectral-measure integral conclusion is not included.
Kaplansky's direct-finiteness conjecture asserts that \(ab=1\) implies \(ba=1\) in every group algebra over a field. Let \(p\) be the smallest prime divisor of \(\bigl(\binom{1200}{600}!\bigr)^2+1\); this prime is odd. The formalized result constructs a field \(K\) of order \(p^4\), a finitely generated group \(G\) with torsion, and elements \(a,b\) violating this implication. The associated cellular automaton on all configurations \(K^G\) is injective but not surjective.
The formalization also contains fixed-field transfer results, separate from the statement linked below.
Comparator links
