Improving Razmyslov's (1974) bound: the Nagata–Higman index is at most n² − 2 for n ≥ 3

Let d(n) be the least m such that every associative (not necessarily unital) algebra over a field of characteristic zero satisfying the identity xn = 0 also satisfies x1x2⋯xm = 0; this is the Nagata–Higman index. Razmyslov proved d(n) ≤ n2 in 1974; Kuzmin proved d(n) ≥ n(n+1)/2 and conjectured equality; this is the Kuzmin (1975) conjecture. We prove d(n) ≤ n2 − 2 for n ≥ 3 (and, by a simpler case of the same method, d(n) ≤ n2 − 1 for n ≥ 2); in particular d(6) ≤ 34. To our knowledge, n = 6 is the first case in which the new bound improves the known bounds, and this is the first improvement of Razmyslov's bound for general n. For m = n2 − 1 and m = n2 − 2, Formanek's criterion reduces d(n) ≤ m to the statement that no nonzero linear combination of (m+1)-cycles lies in one particular isotypic block of the group algebra of Sm+1. For m = n2 − 1 this statement follows from the branching rule; for m = n2 − 2 we prove it using the Jucys–Murphy elements and a theorem of Frobenius on the characters of the alternating group. These bounds have also been proved in the Lean proof assistant. The Lean 4 proof of this paper's results: https://github.com/david44hello/papers_supporting_materials/tree/nagata-higman-index-v1.12/nagata-higman-index.