FormalConjectures.Arxiv.«2605.12342».Conjecture1

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Fernandes' conjecture on the 2-generation of even direct product permutation groups

Reference: arxiv/2605.12342 Groups of permutations that are even on maximal proper subsets, and related monoids by Vítor H. Fernandes

For positive integers $m, n \ge 2$, let $\mathrm{S}_m \times \mathrm{S}n$ be the direct product of symmetric groups on $[m] = {1, \dots, m}$ and $[n'] = {1', \dots, n'}$. Define $$ \Gamma{m \oplus n} = {(\sigma_1, \sigma_2) \in \mathrm{S}_m \times \mathrm{S}_n : \mathrm{sgn}(\sigma_1) = \mathrm{sgn}(\sigma_2)} $$ to be the index-$2$ subgroup of pairs of permutations with equal parity, i.e., those whose product action on $[m] \cup [n']$ is an even permutation.

It is known that $\mathrm{rank}(\Gamma_{2 \oplus 2}) = 1$, $\mathrm{rank}(\Gamma_{3 \oplus 3}) = 3$, $\mathrm{rank}(\Gamma_{4 \oplus 3}) = 3$, and $\mathrm{rank}(\Gamma_{4 \oplus 4}) = 3$.

Conjecture 1 (Fernandes, 2026): For all integers $m \ge n \ge 2$ such that $(m, n) \notin {(2,2), (3,3), (4,3), (4,4)}$, the group $\Gamma_{m \oplus n}$ has rank $2$ (i.e., is $2$-generated).

namespace Arxiv.«2605.12342»open Equiv.Perm

The group homomorphism $(\sigma_1, \sigma_2) \mapsto \mathrm{sgn}(\sigma_1) \cdot \mathrm{sgn}(\sigma_2)^{-1}$ from $\mathrm{S}_m \times \mathrm{S}_n$ to ${+1, -1}$.

Its kernel is exactly $\Gamma_{m \oplus n}$.

noncomputable def signDiffHom (m n : ℕ) : Equiv.Perm (Fin m) × Equiv.Perm (Fin n) →* ℤˣ :=
  (sign.comp (MonoidHom.fst _ _)) * (sign.comp (MonoidHom.snd _ _))⁻¹

The subgroup $\Gamma_{m \oplus n} \le \mathrm{S}_m \times \mathrm{S}_n$ consisting of all pairs $(\sigma_1, \sigma_2)$ of permutations with equal signature, i.e. $\mathrm{sgn}(\sigma_1) = \mathrm{sgn}(\sigma_2)$.

This is the kernel of the sign-difference homomorphism $(\sigma_1, \sigma_2) \mapsto \mathrm{sgn}(\sigma_1) \cdot \mathrm{sgn}(\sigma_2)^{-1}$, and is an index-$2$ subgroup of $\mathrm{S}_m \times \mathrm{S}_n$.

noncomputable def gammaSubgroup (m n : ℕ) : Subgroup (Equiv.Perm (Fin m) × Equiv.Perm (Fin n)) :=
  (signDiffHom m n).ker

Conjecture 1 (Fernandes, 2026): Let $m \ge n \ge 2$ be integers with $(m, n) \notin {(2,2), (3,3), (4,3), (4,4)}$. Then the group $$ \Gamma_{m \oplus n} = {(\sigma_1, \sigma_2) \in \mathrm{S}_m \times \mathrm{S}_n : \mathrm{sgn}(\sigma_1) = \mathrm{sgn}(\sigma_2)} $$ has rank $2$, i.e., minimal generating set of size $2$.

Note: Fernandes states the conjecture for groups of exact rank $2$, which is why $(2,2)$ is in the exception list: $\Gamma_{2 \oplus 2} \cong C_2$ has rank $1$. The formalised conclusion ∃ g₁ g₂, closure {g₁, g₂} = ⊤ encodes 2-generation (at most $2$ generators), which $\Gamma_{2 \oplus 2}$ also satisfies. The other three exceptions $(3,3), (4,3), (4,4)$ have rank $3$ and are genuinely not 2-generated.

@[category research open, AMS 20]
theorem conjecture_1 {m n : ℕ} (hm2 : 2 ≤ m) (hn2 : 2 ≤ n) (hmn : n ≤ m)
    (h_except : (m, n) ∉ ({(2, 2), (3, 3), (4, 3), (4, 4)} : Set (ℕ × ℕ))) :
    ∃ g₁ g₂ : gammaSubgroup m n, Subgroup.closure {g₁, g₂} = ⊤ := bym:ℕn:ℕhm2:2 ≤ mhn2:2 ≤ nhmn:n ≤ mh_except:(m, n) ∉ {(2, 2), (3, 3), (4, 3), (4, 4)}⊢ ∃ g₁ g₂, Subgroup.closure {g₁, g₂} = ⊤
  sorryAll goals completed! 🐙

It is known that $\Gamma_{2 \oplus 2} \cong C_2$ has rank $1$: it is cyclic, generated by a single element.

@[category research solved, AMS 20]
theorem conjecture_1.variants.rank_2_2 :
    ∃ g : gammaSubgroup 2 2, Subgroup.closure {g} = ⊤ := by⊢ ∃ g, Subgroup.closure {g} = ⊤
  sorryAll goals completed! 🐙

It is known that $\Gamma_{3 \oplus 3}$ has rank $3$: it is not $2$-generated.

@[category research solved, AMS 20]
theorem conjecture_1.variants.rank_3_3 :
    ∀ h₁ h₂ : gammaSubgroup 3 3, Subgroup.closure {h₁, h₂} ≠ ⊤ := by⊢ ∀ (h₁ h₂ : ↥(gammaSubgroup 3 3)), Subgroup.closure {h₁, h₂} ≠ ⊤
  sorryAll goals completed! 🐙

It is known that $\Gamma_{4 \oplus 3}$ has rank $3$: it is not $2$-generated.

@[category research solved, AMS 20]
theorem conjecture_1.variants.rank_4_3 :
    ∀ h₁ h₂ : gammaSubgroup 4 3, Subgroup.closure {h₁, h₂} ≠ ⊤ := by⊢ ∀ (h₁ h₂ : ↥(gammaSubgroup 4 3)), Subgroup.closure {h₁, h₂} ≠ ⊤
  sorryAll goals completed! 🐙

It is known that $\Gamma_{4 \oplus 4}$ has rank $3$: it is not $2$-generated.

@[category research solved, AMS 20]
theorem conjecture_1.variants.rank_4_4 :
    ∀ h₁ h₂ : gammaSubgroup 4 4, Subgroup.closure {h₁, h₂} ≠ ⊤ := by⊢ ∀ (h₁ h₂ : ↥(gammaSubgroup 4 4)), Subgroup.closure {h₁, h₂} ≠ ⊤
  sorryAll goals completed! 🐙

end Arxiv.«2605.12342»