The result
Theorem
For a finite group G, a prime p and a multilinear commutator word w, the verbal subgroup w(G) has a normal p-complement if and only if p divides |xy| whenever x and y are w-values with |x| prime to p and p dividing |y|.
Scope of the contribution
All finite groups, all primes and all multilinear commutator words, including the one-variable word. The formal proof assumes Thompson's minimal-simple classification and the published theorem that every element of a finite quasisimple group whose order is coprime to the center's order is a commutator. These two results are explicit hypotheses; their published proofs are not formalized here.
General multilinear-word criterion and conditional formalization
Mathematical dependencies and credit
Additional word and extension arguments, their assembly into the general result, formalization and verification by Nilradical v1.0.0. The original question, earlier cases, structural theorems and reused formal foundations retain their source credits.
- Assumed. Thompson's classification of finite minimal nonabelian simple groups. Source
- Assumed. Coprime-order elements of finite quasisimple groups are commutators (Liebeck–O’Brien–Shalev–Tiep). Source
- Nilradical v1.0.0 — additional word and extension arguments, proof assembly, formalization and verification
- Y. Contreras Rojas, V. Grazian and C. Monetta — original question, earlier cases and centralization argument
- J. G. Thompson — minimal-simple classification
- M. W. Liebeck, E. A. O'Brien, A. Shalev and P. H. Tiep — quasisimple commutator theorem
- Yawara Ishida and the OddOrder, Qiuzhen-CFSG, Tau Ceti, Lean and mathlib contributors — reused mathematics and code
Proof source
The source and theorem endpoints refer to the pinned revision.
Kourovka2135.problem2135_outerWordKourovka2135.problem2135Kourovka2135.productOrderCondition_iff_hasNormalPComplement
Source revisioneb026951d20b1a362c7ec206ac116cd55547e96d
Recorded checks and review
Recorded proof checks
All 745 project modules were built in the protected verification run. The captured exports subsequently passed both Lean and Nanoda, with the frozen-statement comparison and logical-axiom audit authenticated by an independent evidence review. The three endpoints retain the two explicit published mathematical hypotheses described in the scope. Publication reuses this completed verification and does not rebuild or replay the proof. Final human statement acceptance was recorded on 2026-09-21 for the linked proof snapshot.
Statement review
Recorded comparison of the formal statement and its intended mathematical scope.
Human statement acceptance
Human statement acceptance for this pinned source snapshot. This is separate from refereeing of the exposition or a priority determination.
Historical literature review
The bounded literature review distinguishes the general multilinear-word result from the earlier lower-central-word and soluble derived-word cases. No absolute priority claim is made.
Mathematical note
Agent-generated exposition; not refereed, revised . The note does not change the proof statement or its recorded checks.
Read the mathematical noteCite this contribution
Nilradical v1.0.0. A p-nilpotency criterion for word values. Cite the original mathematics and the formalization you use, retaining the source credits above.
BibTeX citation
@misc{nilradical_kourovka_21_35,
author = {{Nilradical}},
title = {A p-nilpotency criterion for word values},
url = {https://github.com/alunik/kourovka-lean/blob/b1d402628777079594abfc27cd05b006b8524543/Kourovka/Problem2135/README.md},
note = {Source revision eb026951d20b1a362c7ec206ac116cd55547e96d}
}Using this contribution does not require adding Nilradical or anyone from the project as a coauthor.