Singularity of mixed identities in oligomorphic permutation groups

### What is the conjecture
Let $\Omega$ be an infinite set and let $G \le \mathrm{Sym}(\Omega)$ be a permutation group. The group $G$ is called **oligomorphic** if for every integer $k \ge 1$, the diagonal action of $G$ on $\Omega^k$ has only finitely many orbits.

Let $F_r$ denote the free group of rank $r$ with free generators $x_1, \dots, x_r$. An element $w \in G * F_r$ of the free product of $G$ and $F_r$ represents a word with constants in $G$, and induces an evaluation map $w \colon G^r \to G$. The word $w$ is called a **mixed identity** of $G$ if $w(g_1, \dots, g_r) = 1_G$ for all $(g_1, \dots, g_r) \in G^r$.

Let $\mathrm{rk} \colon G * F_r \to F_r$ be the natural augmentation homomorphism that maps every element of $G$ to $1_{F_r}$ and acts as the identity on $F_r$. A word $w$ is called **singular** if $\mathrm{rk}(w) = 1_{F_r}$, and **regular** otherwise.

The source paper resolves the conjecture for the large class of permutation groups having no algebraicity (where every point outside a finite subset $B$ has an infinite stabilizer orbit $G_B \cdot a$) and under modular pregeometry conditions. The general problem remains open:

**Conjecture (Bodirsky–Schneider–Thom / Bodirsky et al., 2024):** Let $G \curvearrowright \Omega$ be an oligomorphic permutation group. Then all mixed identities of $G$ are singular (i.e., $G$ satisfies no non-trivial regular mixed identity).

* **Source Paper:** *All mixed identities are singular in groups with no algebraicity* ([arXiv:2606.24741](https://arxiv.org/abs/2606.24741), [HTML](https://arxiv.org/html/2606.24741), [PDF](https://arxiv.org/pdf/2606.24741))
* **Authors:** Paolo Marimon, Michael Pinsker
* **In-Paper Location:** [Conjecture 1.1 (Page 2)](https://arxiv.org/pdf/2606.24741#page=2) in Section 1 "Introduction"
* **OpenConjecture ID:** 4302 ([OpenConjecture](https://github.com/davisrbr/conjectures-arxiv))

### Prerequisites needed
All core group-theoretic structures are available in Mathlib4:
* Free product of groups (coproduct): [`Mathlib.GroupTheory.Coprod.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Coprod/Basic.html)
* Free groups: [`Mathlib.GroupTheory.FreeGroup.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/FreeGroup/Basic.html)
* Group actions and orbits: [`Mathlib.GroupTheory.GroupAction.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/GroupAction/Basic.html)
* Permutations and symmetric groups: [`Mathlib.GroupTheory.Perm.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Basic.html)
* Subgroups: [`Mathlib.Algebra.Group.Subgroup.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Subgroup/Basic.html)

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

This issue was generated by an AI agent and reviewed by me.