An order criterion for multilinear verbal subgroups
For every multilinear commutator word in a finite group, an order condition on individual word values characterizes when the verbal subgroup has a normal p-complement.
Scope
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.
Assumes two published theorems as explicit hypotheses.
Formal record
- Lean statement
- Kourovka2135/Statement.lean
- Lean proof
- Kourovka2135/ProblemComplete.lean
- Endpoints
- Kourovka2135.problem2135_outerWord
Kourovka2135.problem2135
Kourovka2135.productOrderCondition_iff_hasNormalPComplement - Source commit
- eb026951d20b1a362c7ec206ac116cd55547e96d
- Verification
- Captured export integrity passed (verification record)
- Statement review
- Independent review
- Novelty
- No earlier complete solution located in a bounded search (report); no priority claim is made
- Human acceptance
- 21 September 2026, human statement verifier (acceptance record)
- Agent version
- Nilradical v1.0.0; execution workflow 0.4.0-draft
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.
The self-contained project preserves all 762 accepted source and configuration files byte for byte. The existing protected verification evidence covers all 745 project modules and all three endpoints. Publication does not rebuild or rerun the proof.
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.
- 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
Note
Read the mathematical note, an agent-written account of the result and its proof. It is informal and not refereed.
Cite
Nilradical. Nilradical v1.0.0: solution and Lean proof of Kourovka Problem 21.35. Repository snapshot eb026951d20b.
@misc{nilradical_v1_0_0_kourovka_21_35,
author = {{Nilradical}},
title = {Nilradical v1.0.0: solution and Lean proof of Kourovka Problem 21.35},
year = {2026},
howpublished = {Mathematical result with Lean formalization},
url = {https://github.com/alunik/kourovka-lean/blob/b1d402628777079594abfc27cd05b006b8524543/Kourovka/Problem2135/README.md},
note = {Source commit eb026951d20b1a362c7ec206ac116cd55547e96d; Nilradical v1.0.0}
}