Cardinal bounds for cyclic ascent and separation of overnilpotent radicals in 2-groups

For each infinite cardinal \(κ\), we construct a nontrivial \(2\)-group \(G_κ\) in which every cyclic subgroup has a continuous ascending normal series of cardinal length at most \(κ\), but only the identity subgroup has one of cardinal length less than \(κ\). Hence \( R_κ(G_κ)=1\) and \( R_μ(G_κ)=G_κ\) for \(μ>κ\), answering Kourovka Problem 3.43. Extensions by finite quotient orbits of Vovsi's group give the construction. Elementary abelian normal layers bound the ascent lengths, and disjoint commutators exclude shorter series, also at singular cardinals. These results are formalised in Lean 4.