Wilson catalog labels and admissible parameters

import Mathlib.Algebra.Ring.Parity
import Mathlib.Data.Nat.Prime.Defs
import Mathlib.Data.Fintype.Card
import Mathlib.Tactic.DeriveFintype

namespace WilsonCatalog

/-- Wilson's six classical families of finite simple groups.  The rank parameter and
field-size parameter are carried separately by `Label.classical`. -/
inductive ClassicalFamily where
  | projectiveSpecialLinear
  | projectiveSpecialUnitary
  | projectiveSymplectic
  | projectiveOrthogonalOdd
  | projectiveOrthogonalPlus
  | projectiveOrthogonalMinus
  deriving DecidableEq, Fintype, Repr

/-- Wilson's ten exceptional (including twisted) families.  The Tits group is the
small derived member associated with the `reeF4` family, not a sporadic label. -/
inductive ExceptionalFamily where
  | chevalleyG2
  | chevalleyF4
  | chevalleyE6
  | chevalleyE7
  | chevalleyE8
  | twistedE6
  | trialityD4
  | suzukiB2
  | reeG2
  | reeF4
  deriving DecidableEq, Fintype, Repr

/-- The 26 sporadic simple groups in the ATLAS/Wilson convention. -/
inductive SporadicName where
  | mathieu11
  | mathieu12
  | mathieu22
  | mathieu23
  | mathieu24
  | janko1
  | janko2
  | janko3
  | janko4
  | conway1
  | conway2
  | conway3
  | fischer22
  | fischer23
  | fischer24Prime
  | higmanSims
  | mclaughlin
  | held
  | rudvalis
  | suzuki
  | onan
  | haradaNorton
  | lyons
  | thompson
  | babyMonster
  | monster
  deriving DecidableEq, Fintype, Repr

/-- A raw name in Wilson's catalog.  Admissibility restrictions and concrete group
realizations are deliberately separate: this datatype alone asserts neither that a
parameter is valid nor that the named group is finite or simple. -/
inductive Label where
  | primeCyclic (prime : Nat)
  | alternating (degree : Nat)
  | classical (family : ClassicalFamily) (rank fieldSize : Nat)
  | exceptional (family : ExceptionalFamily) (fieldSize : Nat)
  | sporadic (name : SporadicName)
  deriving DecidableEq, Repr

inductive Category where
  | primeCyclic
  | alternating
  | classical
  | exceptional
  | sporadic
  deriving DecidableEq, Fintype, Repr

def Label.category : Label → Category
  | .primeCyclic _ => .primeCyclic
  | .alternating _ => .alternating
  | .classical _ _ _ => .classical
  | .exceptional _ _ => .exceptional
  | .sporadic _ => .sporadic

theorem classical_family_count : Fintype.card ClassicalFamily = 6 := by decide

theorem exceptional_family_count : Fintype.card ExceptionalFamily = 10 := by decide

theorem sporadic_group_count : Fintype.card SporadicName = 26 := by decide

def IsPrimePower (q : Nat) : Prop :=
  ∃ prime exponent : Nat, prime.Prime ∧ 0 < exponent ∧ q = prime ^ exponent

def IsOddPrimePower (q : Nat) : Prop :=
  IsPrimePower q ∧ Odd q

def IsSuzukiParameter (q : Nat) : Prop :=
  ∃ exponent : Nat, 0 < exponent ∧ q = 2 ^ (2 * exponent + 1)

def IsSmallReeParameter (q : Nat) : Prop :=
  ∃ exponent : Nat, 0 < exponent ∧ q = 3 ^ (2 * exponent + 1)

def IsLargeReeParameter (q : Nat) : Prop :=
  q = 2 ∨ IsSuzukiParameter q

/-- The non-simple low-parameter members are excluded.  Repeated isomorphism types are
allowed, except that odd-dimensional orthogonal groups in even characteristic are assigned
to the symplectic family. -/
def ClassicalFamily.IsAdmissible : ClassicalFamily → Nat → Nat → Prop
  | .projectiveSpecialLinear, dimension, q =>
      IsPrimePower q ∧ 2 ≤ dimension ∧ ¬ (dimension = 2 ∧ (q = 2 ∨ q = 3))
  | .projectiveSpecialUnitary, dimension, q =>
      IsPrimePower q ∧ 3 ≤ dimension ∧ ¬ (dimension = 3 ∧ q = 2)
  | .projectiveSymplectic, rank, q =>
      IsPrimePower q ∧ 2 ≤ rank ∧ ¬ (rank = 2 ∧ q = 2)
  | .projectiveOrthogonalOdd, rank, q =>
      IsOddPrimePower q ∧ 3 ≤ rank
  | .projectiveOrthogonalPlus, rank, q =>
      IsPrimePower q ∧ 4 ≤ rank
  | .projectiveOrthogonalMinus, rank, q =>
      IsPrimePower q ∧ 4 ≤ rank

/-- Admissible field sizes for the exceptional and twisted families.  At field size two,
the `reeF4` label denotes the derived Tits group `²F₄(2)'`; larger members use
`q = 2^(2m+1)` with `m > 0`. -/
def ExceptionalFamily.IsAdmissible : ExceptionalFamily → Nat → Prop
  | .chevalleyG2, q => IsPrimePower q ∧ 2 < q
  | .chevalleyF4, q => IsPrimePower q
  | .chevalleyE6, q => IsPrimePower q
  | .chevalleyE7, q => IsPrimePower q
  | .chevalleyE8, q => IsPrimePower q
  | .twistedE6, q => IsPrimePower q
  | .trialityD4, q => IsPrimePower q
  | .suzukiB2, q => IsSuzukiParameter q
  | .reeG2, q => IsSmallReeParameter q
  | .reeF4, q => IsLargeReeParameter q

def Label.IsAdmissible : Label → Prop
  | .primeCyclic prime => prime.Prime
  | .alternating degree => 5 ≤ degree
  | .classical family rank q => family.IsAdmissible rank q
  | .exceptional family q => family.IsAdmissible q
  | .sporadic _ => True

end WilsonCatalog