Kourovka 1.54 - Topology of the Space of Orderings

### What is the conjecture
**Is the space of bi-orderings for a free *metabelian* group also a Cantor set?**

This is a sub-problem of Kourovka Notebook Problem **1.54**: "Describe all linear orderings of a free metabelian group with a finite number of generators."

### Status and Discussion of the general problem in Research Papers
The general problem was proposed by **A. I. Kokorin** in the **1st issue (1965)** of the Kourovka Notebook.

* **Status:** As of the **20th edition (2022)** of the Kourovka Notebook, the problem remains listed in the main section of **unsolved problems**. It does not have a "Solved by..." note attached to it in the official list, implying a complete and satisfactory "description" covering all ranks and types of orderings is considered either open or not yet fully consolidated into a single theorem.
* **Recent Progress (2023):** There is a significant recent paper by **Wenhao Wang** titled **"Orders on free metabelian groups"** (*Journal of Group Theory*, 2023). This paper directly addresses the problem and provides substantial results.
* Wang proves that for a free metabelian group of **rank 2**, the derived subgroup is **convex** with respect to *any* bi-ordering (linear ordering).
* For ranks greater than 2, the paper investigates the convex hull of the derived subgroup.
* The paper also establishes that free metabelian groups are **computably bi-orderable**, but the orders are **never regular** (in the sense of formal language theory) unless the group is cyclic.

### Prerequisites needed
To state the question in Lean 4, you do not need to invent new mathematics, but you must bridge the gap between Mathlib's "typeclass" approach (where a group has *one* fixed order) and the "moduli space" approach (where you consider the set of *all* possible orders).

The following definitions and structures are currently **missing** from Mathlib and would need to be defined to state the problem formally.

### 1. The Space of Bi-Orderings (The Main Gap)
Mathlib has `LinearOrderedGroup G`, which assumes $G$ comes with a single, fixed order. To state the problem, you need to treat the order as a *variable* or a *point* in a space.

**Missing Definition:** A type representing the set of all valid bi-invariant linear orders on a group.
**Missing Structure:** The "Sikora Topology" (or logical topology) on this set.

You would need to define something like this:
```lean
import Mathlib.Algebra.Order.Group.Defs
import Mathlib.Topology.Basic

variable (G : Type*) [Group G]

/-- The type of all bi-invariant linear order relations on G. -/
def BiOrderings := { r : G → G → Prop // IsLinearOrder G r ∧ IsBiInvariant G r }

/-- The "Sikora Topology": The subspace topology induced by the
product topology on 2^(G × G). -/
instance : TopologicalSpace (BiOrderings G) :=
induced (fun r => r.val) inferInstance
```
*Note: Mathlib has the machinery for product topologies (`Pi.topologicalSpace`), but the specific instance restricting it to the subset of valid group orderings is missing.*

### 2. The Free Metabelian Group
Mathlib has `FreeGroup` and general tools for commutators and derived series, but it does not have a specific, pre-packaged definition for `FreeMetabelianGroup`.

**Missing Definition:** A concrete definition of the free metabelian group as a quotient.

You would need to define:
```lean
import Mathlib.GroupTheory.FreeGroup
import Mathlib.GroupTheory.Solvable

/-- The second derived subgroup of the free group (the commutator of the commutator). -/
def FreeMetabelianRel (n : Type*) : Subgroup (FreeGroup n) :=
((FreeGroup n).derivedSeries 2)

/-- The Free Metabelian Group is the Free Group mod its second derived subgroup. -/
def FreeMetabelianGroup (n : Type*) :=
FreeGroup n ⧸ (FreeMetabelianRel n)
```

### 3. The Cantor Set (Available, but Specifics Matter)
Mathlib *does* have definitions for the Cantor set (e.g., `Mathlib.Topology.Instances.CantorSet`), but in the context of this problem, "The Cantor Set" usually refers to the topological type of the space $2^\mathbb{N}$ (or $\mathbb{N} \to \text{Bool}$).

**Status:** **Not Missing.**
You can simply use `ℕ → Bool` equipped with the standard product topology, or use the abstract characterization of a Cantor Space (compact, perfect, totally disconnected, metrizable, non-empty).

---

### Summary of What You Must Write
To state the question **"Is the space of bi-orderings for a free metabelian group homeomorphic to the Cantor set?"**, you would need to write the following statement in Lean, after filling in the definitions above:

```lean
/-- The Formal Question -/
def IsCantorSpace (X : Type*) [TopologicalSpace X] : Prop :=
Nonempty (X ≃ₜ (ℕ → Bool)) -- Is X homeomorphic to the standard Cantor set?

theorem OpenProblem_1_54 (n : ℕ) (h : n ≥ 2) :
IsCantorSpace (BiOrderings (FreeMetabelianGroup (Fin n))) :=
sorry
```

**In short:** The logic and topology libraries are ready; you essentially just need to bundle the concept of "an order relation" into a subtype to apply topology to it.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-06

### 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