FormalConjectures/Arxiv/2605.12342/Conjecture1.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

7 declarations, 5 contain sorry, 0 declared as axioms

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 Reference:

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).

Imports (1)
  1. def Arxiv.«2605.12342».signDiffHom 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\}$ line 60 source

    Source documentation

    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}$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, MonoidHom, Prod, Equiv.Perm, Fin, Units, Int

    Proof uses: HMul.hMul, MonoidHom.comp, Equiv.Perm.sign, MonoidHom.fst, Inv.inv, MonoidHom.snd

    24 instances, coercions and auxiliary constants left out.

    noncomputable def signDiffHom (m n : ℕ) : Equiv.Perm (Fin m) × Equiv.Perm (Fin n) →* ℤˣ :=
…
  2. def Arxiv.«2605.12342».gammaSubgroup Documented declaration: gammaSubgroup line 72 source

    Source documentation

    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$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Subgroup, Prod, Equiv.Perm, Fin

    Proof uses: MonoidHom.ker, Units, Int, Arxiv.«2605.12342».signDiffHom

    6 instances, coercions and auxiliary constants left out.

    noncomputable def gammaSubgroup (m n : ℕ) : Subgroup (Equiv.Perm (Fin m) × Equiv.Perm (Fin n)) :=
…
  3. theorem Arxiv.«2605.12342».conjecture_1 sorry line 96 source

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Not, Membership.mem, Prod, Set, Insert.insert, Prod.mk, Singleton.singleton, Exists, Subtype, Equiv.Perm, Fin, Subgroup, Arxiv.«2605.12342».gammaSubgroup, Eq, Subgroup.closure, Top.top

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  4. theorem Arxiv.«2605.12342».conjecture_1.variants.rank_2_2 It is known that $\Gamma_{2 \oplus 2} \cong C_2$ has rank $1$: it is cyclic, generated by a single element sorry line 106 source

    Source documentation

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

    depends on sorry what this means

    Statement uses: Exists, Subtype, Prod, Equiv.Perm, Fin, OfNat.ofNat, Nat, Membership.mem, Subgroup, Arxiv.«2605.12342».gammaSubgroup, Eq, Subgroup.closure, Singleton.singleton, Set, Top.top

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem conjecture_1.variants.rank_2_2 :
    ∃ g : gammaSubgroup 2 2, Subgroup.closure {g} = ⊤ := by
…

    Mentions: Arxiv.«2605.12342».gammaSubgroup

  5. theorem Arxiv.«2605.12342».conjecture_1.variants.rank_3_3 It is known that $\Gamma_{3 \oplus 3}$ has rank $3$: it is not $2$-generated sorry line 114 source

    Source documentation

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

    depends on sorry what this means

    Statement uses: Subtype, Prod, Equiv.Perm, Fin, OfNat.ofNat, Nat, Membership.mem, Subgroup, Arxiv.«2605.12342».gammaSubgroup, Ne, Subgroup.closure, Insert.insert, Set, Singleton.singleton, Top.top

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem conjecture_1.variants.rank_3_3 :
    ∀ h₁ h₂ : gammaSubgroup 3 3, Subgroup.closure {h₁, h₂} ≠ ⊤ := by
…

    Mentions: Arxiv.«2605.12342».gammaSubgroup

  6. theorem Arxiv.«2605.12342».conjecture_1.variants.rank_4_3 It is known that $\Gamma_{4 \oplus 3}$ has rank $3$: it is not $2$-generated sorry line 122 source

    Source documentation

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

    depends on sorry what this means

    Statement uses: Subtype, Prod, Equiv.Perm, Fin, OfNat.ofNat, Nat, Membership.mem, Subgroup, Arxiv.«2605.12342».gammaSubgroup, Ne, Subgroup.closure, Insert.insert, Set, Singleton.singleton, Top.top

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem conjecture_1.variants.rank_4_3 :
    ∀ h₁ h₂ : gammaSubgroup 4 3, Subgroup.closure {h₁, h₂} ≠ ⊤ := by
…

    Mentions: Arxiv.«2605.12342».gammaSubgroup

  7. theorem Arxiv.«2605.12342».conjecture_1.variants.rank_4_4 It is known that $\Gamma_{4 \oplus 4}$ has rank $3$: it is not $2$-generated sorry line 130 source

    Source documentation

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

    depends on sorry what this means

    Statement uses: Subtype, Prod, Equiv.Perm, Fin, OfNat.ofNat, Nat, Membership.mem, Subgroup, Arxiv.«2605.12342».gammaSubgroup, Ne, Subgroup.closure, Insert.insert, Set, Singleton.singleton, Top.top

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem conjecture_1.variants.rank_4_4 :
    ∀ h₁ h₂ : gammaSubgroup 4 4, Subgroup.closure {h₁, h₂} ≠ ⊤ := by
…

    Mentions: Arxiv.«2605.12342».gammaSubgroup