Kourovka 2.6

### What is the conjecture
**In an NR-group, the set of generalized central elements coincides with the nil-kernel. Is the converse true, that is, must a group be an NR-group if the set of generalized central elements coincides with the nil-kernel?**

**Status:**
The problem is **unsolved (open)**. It is listed in the "Problems from the 2nd Issue" section of recent editions (e.g., the 19th edition in 2019 and the 20th edition in 2022) without a solution or reference to a paper solving it.

**Clarification of Terminology:**
* **NR-group:** Defined in Problem 2.5 (by Plotkin) as a group where the set of **nil-elements** (Engel elements, denoted $R(G)$) coincides with the **locally nilpotent radical** (Hirsch-Plotkin radical, denoted $\rho(G)$).
* **Generalized central elements:** This refers to the elements of the **hypercenter** (or upper central series), denoted $\zeta(G)$ or $ZA(G)$.
* **Nil-kernel:** In the context of Plotkin and Vilyatser's work (e.g., *Groups of Automorphisms of Algebraic Systems*), the nil-kernel of a group acting on itself (inner automorphisms) is the set of elements acting nilpotently. This is exactly the set of **Right Engel elements** ($R(G)$).

See also #1940.

**Mathematical Interpretation:**
Vilyatser asserts that in an NR-group (where $R(G) = \rho(G)$), it is also true that $\zeta(G) = R(G)$. (This implies that in an NR-group, the Hirsch-Plotkin radical is hypercentral).
The problem asks for the converse: **If the set of Engel elements coincides with the hypercenter ($R(G) = \zeta(G)$), does it follow that the group is an NR-group (i.e., $R(G) = \rho(G)$)?**
Since $\zeta(G) \subseteq \rho(G)$ is always true, and the hypothesis is $R(G) = \zeta(G)$, the question essentially asks: **Does $R(G) = \zeta(G)$ imply $\rho(G) = \zeta(G)$?** (i.e., if the Engel elements are precisely the hypercentral ones, is the locally nilpotent radical also hypercentral?)

**Discussion in Research:**
The problem is not widely discussed in recent English-language research papers outside of being listed in the Kourovka Notebook. It belongs to the specific line of investigation into "Radical Groups" and "Automorphism Groups" pursued by the Plotkin school in the 1960s and 70s. While relationships between $R(G)$, $\zeta(G)$, and $\rho(G)$ are studied (e.g., in Noetherian groups, they coincide), this specific implication remains an open question in the general case.

### Prerequisites needed
To state Kourovka Problem 2.6 in Lean 4, you need the definitions from Problem 2.5 (#1940, Engel elements and Hirsch-Plotkin radical) plus one significant new structure: the **Hypercenter** (transfinite upper central series).

Here are the specific definitions and structures missing from **mathlib**:

### 1. The Set of Right Engel Elements ("Nil-kernel")
As with Problem 2.5, mathlib has `IsNilpotent`, but it lacks the specific set definition for Right Engel elements. In the context of this problem (Vilyatser/Plotkin), the "nil-kernel" refers to this set.
* **Missing Definition:** `RightEngelSet G : Set G`
$$ \{ g \in G \mid \forall x \in G, \exists n \in \mathbb{N}, [x, {_n} g] = 1 \} $$

### 2. Locally Nilpotent Radical ("Hirsch-Plotkin Radical")
Necessary to define an "NR-group". Mathlib has nilpotent groups, but not the specific machinery for local nilpotency.
* **Missing Predicate:** `IsLocallyNilpotent G` (Every finitely generated subgroup is nilpotent).
* **Missing Definition:** `HirschPlotkinRadical G` (The supremum of all normal locally nilpotent subgroups).

### 3. The Hypercenter ("Generalized Central Elements")
Problem 2.6 refers to "generalized central elements." In group theory, these are the elements belonging to the **Hypercenter** (the stationary limit of the upper central series).
* **Current Mathlib Status:** Mathlib contains `upperCentralSeries`, but it is indexed by natural numbers ($\mathbb{N}$). This is sufficient only for nilpotent groups.
* **Missing Structure:** The **Transfinite Upper Central Series**. You need to define the series indexed by ordinals:
* $Z_0 = 1$
* $Z_{\alpha+1} / Z_\alpha = Z(G / Z_\alpha)$
* $Z_\lambda = \bigcup_{\beta < \lambda} Z_\beta$ for limit ordinals.
* **Missing Definition:** `Hypercenter G` (or `GeneralizedCenter G`). This is the union of all terms in the transfinite series (or the term where the series stabilizes).

### 4. NR-Group
* **Missing Definition:** A predicate defining a group where the `RightEngelSet` equals the `HirschPlotkinRadical`.

### Summary for Implementation
To state the question `RightEngelSet G = Hypercenter G \to IsNRGroup G`, you must manually implement the **transfinite recursion** required to define the Hypercenter, as mathlib currently focuses on finite compositions for nilpotency.
### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-20

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [X] This issue is up for grabs: I would like to see this conjecture added by somebody else