Order formula for a Wilson-catalog label

import Definitions.Def_wilson_catalog_labels
import Mathlib

namespace CFSG

open WilsonCatalog

/-- The known order of a classical family member, following the closed-form product
formulas tabulated in Wilson, *The Finite Simple Groups*, Ch. 3. Values are computed
by exact integer division; the divisor is known to divide the numerator whenever
`family.IsAdmissible rank fieldSize` holds. -/
def classicalOrder (family : ClassicalFamily) (rank q : Nat) : Nat :=
  match family with
  | .projectiveSpecialLinear =>
      (q ^ (rank * (rank - 1) / 2) * (Finset.Ico 2 (rank + 1)).prod (fun i => q ^ i - 1))
        / Nat.gcd rank (q - 1)
  | .projectiveSpecialUnitary =>
      (q ^ (rank * (rank - 1) / 2) *
        (Finset.Ico 2 (rank + 1)).prod (fun i => if i % 2 = 0 then q ^ i - 1 else q ^ i + 1))
        / Nat.gcd rank (q + 1)
  | .projectiveSymplectic =>
      (q ^ (rank ^ 2) * (Finset.Ico 1 (rank + 1)).prod (fun i => q ^ (2 * i) - 1))
        / Nat.gcd 2 (q - 1)
  | .projectiveOrthogonalOdd =>
      (q ^ (rank ^ 2) * (Finset.Ico 1 (rank + 1)).prod (fun i => q ^ (2 * i) - 1))
        / Nat.gcd 2 (q - 1)
  | .projectiveOrthogonalPlus =>
      (q ^ (rank * (rank - 1)) * (q ^ rank - 1) *
        (Finset.Ico 1 rank).prod (fun i => q ^ (2 * i) - 1))
        / Nat.gcd 4 (q ^ rank - 1)
  | .projectiveOrthogonalMinus =>
      (q ^ (rank * (rank - 1)) * (q ^ rank + 1) *
        (Finset.Ico 1 rank).prod (fun i => q ^ (2 * i) - 1))
        / Nat.gcd 4 (q ^ rank + 1)

/-- The known order of an exceptional (Chevalley or twisted) family member, following
Wilson, *The Finite Simple Groups*, Ch. 4. The field-size-two member of `reeF4` denotes
the derived Tits group `²F₄(2)'`, whose order is half the generic formula's value. -/
def exceptionalOrder (family : ExceptionalFamily) (q : Nat) : Nat :=
  match family with
  | .chevalleyG2 => q ^ 6 * (q ^ 6 - 1) * (q ^ 2 - 1)
  | .chevalleyF4 => q ^ 24 * (q ^ 12 - 1) * (q ^ 8 - 1) * (q ^ 6 - 1) * (q ^ 2 - 1)
  | .chevalleyE6 =>
      (q ^ 36 * (q ^ 12 - 1) * (q ^ 9 - 1) * (q ^ 8 - 1) * (q ^ 6 - 1) * (q ^ 5 - 1) * (q ^ 2 - 1))
        / Nat.gcd 3 (q - 1)
  | .chevalleyE7 =>
      (q ^ 63 * (q ^ 18 - 1) * (q ^ 14 - 1) * (q ^ 12 - 1) * (q ^ 10 - 1) * (q ^ 8 - 1) *
        (q ^ 6 - 1) * (q ^ 2 - 1)) / Nat.gcd 2 (q - 1)
  | .chevalleyE8 =>
      q ^ 120 * (q ^ 30 - 1) * (q ^ 24 - 1) * (q ^ 20 - 1) * (q ^ 18 - 1) * (q ^ 14 - 1) *
        (q ^ 12 - 1) * (q ^ 8 - 1) * (q ^ 2 - 1)
  | .twistedE6 =>
      (q ^ 36 * (q ^ 12 - 1) * (q ^ 9 + 1) * (q ^ 8 - 1) * (q ^ 6 - 1) * (q ^ 5 + 1) * (q ^ 2 - 1))
        / Nat.gcd 3 (q + 1)
  | .trialityD4 => q ^ 12 * (q ^ 8 + q ^ 4 + 1) * (q ^ 6 - 1) * (q ^ 2 - 1)
  | .suzukiB2 => q ^ 2 * (q ^ 2 + 1) * (q - 1)
  | .reeG2 => q ^ 3 * (q ^ 3 + 1) * (q - 1)
  | .reeF4 =>
      let generic := q ^ 12 * (q ^ 6 + 1) * (q ^ 4 - 1) * (q ^ 3 + 1) * (q - 1)
      if q = 2 then generic / 2 else generic

/-- The known order of each of the 26 ATLAS sporadic simple groups, as tabulated in the
ATLAS of Finite Groups. Recorded as an explicit prime factorisation to keep transcription
checkable digit-by-digit against the source rather than as a bare 20-to-54-digit numeral. -/
def sporadicOrder : SporadicName → Nat
  | .mathieu11 => 2 ^ 4 * 3 ^ 2 * 5 * 11
  | .mathieu12 => 2 ^ 6 * 3 ^ 3 * 5 * 11
  | .mathieu22 => 2 ^ 7 * 3 ^ 2 * 5 * 7 * 11
  | .mathieu23 => 2 ^ 7 * 3 ^ 2 * 5 * 7 * 11 * 23
  | .mathieu24 => 2 ^ 10 * 3 ^ 3 * 5 * 7 * 11 * 23
  | .janko1 => 2 ^ 3 * 3 * 5 * 7 * 11 * 19
  | .janko2 => 2 ^ 7 * 3 ^ 3 * 5 ^ 2 * 7
  | .janko3 => 2 ^ 7 * 3 ^ 5 * 5 * 17 * 19
  | .janko4 => 2 ^ 21 * 3 ^ 3 * 5 * 7 * 11 ^ 3 * 23 * 29 * 31 * 37 * 43
  | .conway1 => 2 ^ 21 * 3 ^ 9 * 5 ^ 4 * 7 ^ 2 * 11 * 13 * 23
  | .conway2 => 2 ^ 18 * 3 ^ 6 * 5 ^ 3 * 7 * 11 * 23
  | .conway3 => 2 ^ 10 * 3 ^ 7 * 5 ^ 3 * 7 * 11 * 23
  | .fischer22 => 2 ^ 17 * 3 ^ 9 * 5 ^ 2 * 7 * 11 * 13
  | .fischer23 => 2 ^ 18 * 3 ^ 13 * 5 ^ 2 * 7 * 11 * 13 * 17 * 23
  | .fischer24Prime => 2 ^ 21 * 3 ^ 16 * 5 ^ 2 * 7 ^ 3 * 11 * 13 * 17 * 23 * 29
  | .higmanSims => 2 ^ 9 * 3 ^ 2 * 5 ^ 3 * 7 * 11
  | .mclaughlin => 2 ^ 7 * 3 ^ 6 * 5 ^ 3 * 7 * 11
  | .held => 2 ^ 10 * 3 ^ 3 * 5 ^ 2 * 7 ^ 3 * 17
  | .rudvalis => 2 ^ 14 * 3 ^ 3 * 5 ^ 3 * 7 * 13 * 29
  | .suzuki => 2 ^ 13 * 3 ^ 7 * 5 ^ 2 * 7 * 11 * 13
  | .onan => 2 ^ 9 * 3 ^ 4 * 5 * 7 ^ 3 * 11 * 19 * 31
  | .haradaNorton => 2 ^ 14 * 3 ^ 6 * 5 ^ 6 * 7 * 11 * 19
  | .lyons => 2 ^ 8 * 3 ^ 7 * 5 ^ 6 * 7 * 11 * 31 * 37 * 67
  | .thompson => 2 ^ 15 * 3 ^ 10 * 5 ^ 3 * 7 ^ 2 * 13 * 19 * 31
  | .babyMonster => 2 ^ 41 * 3 ^ 13 * 5 ^ 6 * 7 ^ 2 * 11 * 13 * 17 * 19 * 23 * 31 * 47
  | .monster =>
      2 ^ 46 * 3 ^ 20 * 5 ^ 9 * 7 ^ 6 * 11 ^ 2 * 13 ^ 3 * 17 * 19 * 23 * 29 * 31 * 41 * 47 * 59 * 71

/-- The order that CFSG assigns to an admissible Wilson-catalog label: `p` for a prime
cyclic group, `n!/2` for an alternating group of degree `n`, and the tabulated closed-form
or ATLAS order for a classical, exceptional, or sporadic label. -/
def Label.order : Label → Nat
  | .primeCyclic p => p
  | .alternating n => Nat.factorial n / 2
  | .classical family rank q => classicalOrder family rank q
  | .exceptional family q => exceptionalOrder family q
  | .sporadic name => sporadicOrder name

end CFSG