/-
Copyright 2026 The Monstrous Moonshine formalization authors.
Released under the Apache License 2.0.

# The Coxeter group `Y₄₄₃`

This file formalizes the Coxeter group from which the Fischer--Griess monster is obtained, in
the form used by the Lean 3 project
[`formalabstracts`](https://github.com/formalabstracts/formalabstracts):

```lean
noncomputable def Y443 : Group := coxeter_group $ matrix_of_graph (coxeter_edges [4,4,3])
```

(`src/group_theory/monster.lean`, line 16), with the definitions in
`src/group_theory/presentation.lean`

```lean
def coxeter_group {α} (m : α → α → enat) : Group :=
  ⟪α | set.range (λ x : α × α, (⟪x.1⟫ * ⟪x.2⟫) ^ (m x.1 x.2))⟫

def matrix_of_graph {α} [decidable_eq α] (E : α → α → Prop) [decidable_rel E] (x y : α) : enat :=
  if x = y then 1 else if E x y then 3 else 2

inductive coxeter_vertices {n} (xs : dvector ℕ+ n) : Type
| torso {} : coxeter_vertices
| arm : ∀ x : dfin n, dfin (xs.nth'' x) → coxeter_vertices

inductive coxeter_edges_directed {n} (xs : dvector ℕ+ n) : coxeter_vertices xs → coxeter_vertices xs → Prop
| edge_torso : ∀ i : dfin n, coxeter_edges_directed torso (arm i dfin.fz')
| edge_arm : ∀ i : dfin n, ∀ v : dfin (xs.nth'' i), v.to_nat + 1 ≠ xs.nth'' i →
    coxeter_edges_directed (arm i v) (arm i (v+1))

def coxeter_edges {n} (xs : dvector ℕ+ n) := symmetric_closure (coxeter_edges_directed xs)
```

Two facts about this definition are essential, and neither is what the notation `[4,4,3]` might
suggest.  Both were read off the primary source:

1. **The annotations in `[4,4,3]` are discarded.**  `monster.lean` calls `matrix_of_graph`,
   whose off-diagonal value is always `3` on an edge and `2` otherwise.  The function
   `matrix_of_annotated_graph`, which *does* consult the annotation, is defined in the same
   file `presentation.lean` but is never called by `monster.lean`.  So `[4,4,3]` determines
   only the *arm lengths*; every bond is labelled `3`.  (Confirmed independently by the
   comment at the top of `monster.lean`: "11 relators of the form `(xy)^3=1`, one for each
   pair of adjacent nodes" — a single label, not three different ones.)
2. **There are 12 nodes, not 9.**  `coxeter_vertices [4,4,3]` is a torso together with arms
   of length `4`, `4` and `3`, and `1 + 4 + 4 + 3 = 12`, matching the same comment's
   "12 relators of the form `x^2=1`, one for each node".  The bonds number
   `1 + 3 + 3 + 2 = 11`, matching "11 relators of the form `(xy)^3=1`", and the remaining
   `C(12,2) - 11 = 55` pairs are the commutators, matching "55 relators of the form
   `(xy)^2=1`".

The generators of the spider relation in `monster.lean` are

```lean
private def a  : Y443 := generated_of torso
private def b₁ : Y443 := generated_of $ arm (by to_dfin 0) (by to_dfin 0)
private def c₁ : Y443 := generated_of $ arm (by to_dfin 0) (by to_dfin 1)
-- ... b₂ c₂ (arm 1), b₃ c₃ (arm 2)
noncomputable def spider : Y443 := (a * b₁ * c₁ * a * b₂ * c₂ * a * b₃ * c₃)^10
```

so `a` is the torso and `bᵢ`, `cᵢ` are the first two nodes of the `i`-th arm.  These appear
below as `MM.y443A`, `MM.y443B`, `MM.y443C` and `MM.y443Spider`, ready for the next task (S2),
which quotients by the spider relation and then by the centre to obtain the monster.

## Implementation note

The vertices are a `torso` plus a dependent `arm i v` with `v : Fin (Y443Arms i)`.  To make
`Decidable` actually *compute* on the bond relation, the relation `Y443EdgeD` is proved
equivalent to a `Bool`-valued function `Y443EdgeBool` whose comparisons are on `Nat`s rather
than on `Fin`s, and the `Decidable` instance is transferred across that equivalence.  This is
what makes `decide` work for the counting theorems below (`Y443Vertex_card`,
`Y443EdgeD_card`, `Y443Matrix_multiset`); deciding the relation directly gets stuck on the
proof components of the `Fin` terms.
-/

import Mathlib

noncomputable section

open scoped Classical

namespace MM

/-! ## The vertices -/

/-- The arm lengths of `Y₄₄₃`: the three components of the Lean 3 vector `[4,4,3]`. -/
def Y443Arms : Fin 3 → ℕ
  | ⟨0, _⟩ => 4
  | ⟨1, _⟩ => 4
  | ⟨_, _⟩ => 3

@[simp] theorem Y443Arms_zero : Y443Arms 0 = 4 := rfl
@[simp] theorem Y443Arms_one : Y443Arms 1 = 4 := rfl
@[simp] theorem Y443Arms_two : Y443Arms 2 = 3 := rfl

theorem Y443Arms_pos (i : Fin 3) : 0 < Y443Arms i := by fin_cases i <;> decide

/-- The twelve vertices of `Y₄₄₃`, mirroring `coxeter_vertices [4,4,3]`: a torso (the centre
node) together with three arms of length `4`, `4`, `3`.

The first two nodes of each arm are the nodes called `bᵢ` and `cᵢ` in `monster.lean`. -/
inductive Y443Vertex : Type where
  /-- the centre node, `torso` of the Lean 3 source -/
  | torso : Y443Vertex
  /-- the `v`-th node of arm `i`, `arm i v` of the Lean 3 source -/
  | arm : (i : Fin 3) → Fin (Y443Arms i) → Y443Vertex
  deriving DecidableEq

/-- A copy of `Y443Vertex` with a `Fintype` instance derived by the kernel.  The `Fintype`
instance for `Y443Vertex` below is transported across the evident equivalence, so that
`Finset.univ` enumerates the twelve vertices in an order the kernel can compute with. -/
inductive Y443VertexF : Type where
  | torso : Y443VertexF
  | arm : (i : Fin 3) → Fin (Y443Arms i) → Y443VertexF
  deriving DecidableEq, Fintype

/-- The torso, i.e. the node called `a` in `monster.lean`. -/
abbrev Y443Torso : Y443Vertex := Y443Vertex.torso

/-- The first node of arm `i`, i.e. the node called `bᵢ` in `monster.lean`. -/
abbrev Y443BNode (i : Fin 3) : Y443Vertex := Y443Vertex.arm i ⟨0, Y443Arms_pos i⟩

/-- The second node of arm `i`, i.e. the node called `cᵢ` in `monster.lean`. -/
abbrev Y443CNode (i : Fin 3) : Y443Vertex :=
  Y443Vertex.arm i ⟨1, by have := Y443Arms_pos i; fin_cases i <;> decide⟩

theorem Y443Vertex_toF_ofF (x : Y443VertexF) :
    (match x with
      | .torso => Y443Vertex.torso
      | .arm i v => Y443Vertex.arm i v) = (match x with
      | .torso => Y443Vertex.torso
      | .arm i v => Y443Vertex.arm i v) := rfl

instance : Fintype Y443Vertex := Fintype.ofEquiv Y443VertexF {
  toFun := fun x => match x with
    | .torso => Y443VertexF.torso
    | .arm i v => Y443VertexF.arm i v
  invFun := fun x => match x with
    | .torso => Y443Vertex.torso
    | .arm i v => Y443Vertex.arm i v
  left_inv := by intro x; cases x <;> rfl
  right_inv := by intro x; cases x <;> rfl }

/-- The twelve vertices number twelve. -/
theorem Y443Vertex_card : Fintype.card Y443Vertex = 12 := by decide

/-! ## The bonds -/

/-- The *directed* bonds of `Y₄₄₃`, exactly the two constructors of `coxeter_edges_directed`:
the torso is joined to the first node of each arm, and consecutive nodes of an arm are joined. -/
inductive Y443EdgeD : Y443Vertex → Y443Vertex → Prop where
  | torso (i : Fin 3) : Y443EdgeD Y443Vertex.torso (Y443BNode i)
  | arm (i : Fin 3) (v : Fin (Y443Arms i)) (h : v.val + 1 < Y443Arms i) :
      Y443EdgeD (Y443Vertex.arm i v) (Y443Vertex.arm i ⟨v.val + 1, h⟩)

/-- The `Bool`-valued form of `Y443EdgeD`, comparing `Nat`s so that it computes. -/
def Y443EdgeBool : Y443Vertex → Y443Vertex → Bool
  | .torso, .arm i v => decide (v.val = 0)
  | .arm i v, .arm j w => decide (i = j) && decide (w.val = v.val + 1)
  | _, _ => false

theorem Y443EdgeBool_torso (y : Y443Vertex) :
    Y443EdgeBool Y443Vertex.torso y = true ↔ Y443EdgeD Y443Vertex.torso y := by
  cases y with
  | torso => exact ⟨fun h => absurd h (by decide), fun h => by cases h⟩
  | arm i v =>
      show decide (v.val = 0) = true ↔ Y443EdgeD Y443Vertex.torso (Y443Vertex.arm i v)
      rw [decide_eq_true_eq]
      exact ⟨fun hv => by
          have h : v = ⟨0, Y443Arms_pos i⟩ := Fin.ext hv
          rw [h]; exact Y443EdgeD.torso i,
        fun h => by cases h with | torso j => rfl⟩

theorem Y443EdgeBool_arm (i j : Fin 3) (v : Fin (Y443Arms i)) (w : Fin (Y443Arms j)) :
    Y443EdgeBool (Y443Vertex.arm i v) (Y443Vertex.arm j w) = true ↔
      Y443EdgeD (Y443Vertex.arm i v) (Y443Vertex.arm j w) := by
  show (decide (i = j) && decide (w.val = v.val + 1)) = true ↔ _
  rw [Bool.and_eq_true, decide_eq_true_eq, decide_eq_true_eq]
  constructor
  · rintro ⟨hij, hw⟩
    subst hij
    have hlt : v.val + 1 < Y443Arms i := by have := w.isLt; omega
    have h : w = ⟨v.val + 1, hlt⟩ := Fin.ext hw
    rw [h]; exact Y443EdgeD.arm i v hlt
  · intro h
    cases h with
    | arm k u hu => exact ⟨rfl, rfl⟩

theorem Y443EdgeBool_not_torso (y : Y443Vertex) : Y443EdgeBool y Y443Vertex.torso = false := by
  cases y <;> rfl

theorem Y443EdgeBool_iff (x y : Y443Vertex) : Y443EdgeBool x y = true ↔ Y443EdgeD x y := by
  match x, y with
  | .torso, .torso => exact ⟨fun h => absurd h (by decide), fun h => by cases h⟩
  | .torso, .arm i v => exact Y443EdgeBool_torso _
  | .arm i v, .torso =>
      exact ⟨fun h => absurd (h ▸ Y443EdgeBool_not_torso (Y443Vertex.arm i v)) (by decide),
        fun h => by cases h⟩
  | .arm i v, .arm j w => exact Y443EdgeBool_arm i j v w

instance : DecidableRel Y443EdgeD :=
  fun x y => decidable_of_iff (Y443EdgeBool x y = true) (Y443EdgeBool_iff x y)

/-- The bonds of `Y₄₄₃`: the symmetric closure of `Y443EdgeD`, exactly as
`coxeter_edges = symmetric_closure ∘ coxeter_edges_directed`. -/
def Y443Edge (x y : Y443Vertex) : Prop := Y443EdgeD x y ∨ Y443EdgeD y x

instance : DecidableRel Y443Edge := fun x y =>
  inferInstanceAs (Decidable (Y443EdgeD x y ∨ Y443EdgeD y x))

theorem Y443Edge_symm {x y : Y443Vertex} (h : Y443Edge x y) : Y443Edge y x := h.symm

/-- The bond relation is irreflexive: `Y₄₄₃` has no loops, so no Coxeter relation
`(sᵢ sᵢ)^3 = 1` is imposed that is not already `sᵢ^2 = 1`. -/
theorem Y443Edge_irrefl (x : Y443Vertex) : ¬ Y443Edge x x := by
  intro h
  cases h with
  | inl h1 => cases h1 <;> decide
  | inr h2 => cases h2 <;> decide

/-- The number of *directed* bonds: `3` from the torso plus `3 + 3 + 2` along the arms. -/
theorem Y443EdgeD_card :
    ((Finset.univ : Finset (Y443Vertex × Y443Vertex)).filter
      (fun p => Y443EdgeD p.1 p.2)).card = 11 := by decide

/-- The bond relation has `22` ordered pairs, i.e. `11` bonds, matching the reference's
"11 relators of the form `(xy)^3=1`". -/
theorem Y443Edge_card :
    ((Finset.univ : Finset (Y443Vertex × Y443Vertex)).filter
      (fun p => Y443Edge p.1 p.2)).card = 22 := by decide

/-! ## The Coxeter matrix -/

/-- The entry function of `matrix_of_graph (coxeter_edges [4,4,3])`: `1` on the diagonal, `3`
across a bond, and `2` for a non-adjacent pair.  This is the Lean 3 definition verbatim; note
that it *ignores* the annotations of `[4,4,3]`. -/
def Y443Entry (x y : Y443Vertex) : ℕ :=
  if x = y then 1 else if Y443Edge x y then 3 else 2

@[simp] theorem Y443Entry_self (x : Y443Vertex) : Y443Entry x x = 1 := by
  unfold Y443Entry
  rw [if_pos rfl]

theorem Y443Entry_of_ne {x y : Y443Vertex} (h : x ≠ y) :
    Y443Entry x y = if Y443Edge x y then 3 else 2 := by
  unfold Y443Entry
  rw [if_neg h]

theorem Y443Entry_of_edge {x y : Y443Vertex} (h : Y443Edge x y) : Y443Entry x y = 3 := by
  have hne : x ≠ y := fun hc => Y443Edge_irrefl x (hc ▸ h)
  rw [Y443Entry_of_ne hne, if_pos h]

/-- The Coxeter matrix of `Y₄₄₃`: the formalization of
`matrix_of_graph (coxeter_edges [4,4,3])`. -/
def Y443Matrix : CoxeterMatrix Y443Vertex where
  M := Matrix.of Y443Entry
  isSymm := Matrix.IsSymm.ext fun i j => by
    show Y443Entry j i = Y443Entry i j
    by_cases h : i = j
    · subst h; rw [Y443Entry_self, Y443Entry_self]
    · rw [Y443Entry_of_ne (Ne.symm h), Y443Entry_of_ne h]
      by_cases he : Y443Edge i j
      · rw [if_pos he, if_pos (Y443Edge_symm he)]
      · rw [if_neg he, if_neg (fun hc => he (Y443Edge_symm hc))]
  diagonal := fun i => Y443Entry_self i
  off_diagonal := fun i j hij => by
    rw [Y443Entry_of_ne hij]
    by_cases he : Y443Edge i j <;> simp [he]

/-- `Matrix.of` is not definitionally the identity on entries, so this bridge lemma is needed
for every concrete evaluation of `Y443Matrix`. -/
@[simp] theorem Y443Matrix_apply (i j : Y443Vertex) : Y443Matrix.M i j = Y443Entry i j :=
  Matrix.of_apply ..

/-! ## The multiset of all `144` entries

The decisive check on the definition: the `12 × 12` matrix of `Y₄₄₃` has `12` diagonal entries
`1`, `22 = 2 * 11` entries `3` (one ordered pair for each of the `11` bonds), and
`110 = 144 - 12 - 22` entries `2`.  The statement is about the actual entries of
`Y443Matrix`, so it cannot be satisfied vacuously. -/

theorem Y443Matrix_multiset :
    (Finset.univ.val.map (fun p : Y443Vertex × Y443Vertex => Y443Matrix.M p.1 p.2)) =
      (Multiset.replicate 12 1 + Multiset.replicate 22 3 + Multiset.replicate 110 2 :
        Multiset ℕ) := by decide

theorem Y443Matrix_multiset_card :
    (Finset.univ.val.map (fun p : Y443Vertex × Y443Vertex => Y443Matrix.M p.1 p.2)).card = 144 := by
  rw [Y443Matrix_multiset]
  simp

/-! ## The Coxeter group and its generators -/

/-- The Coxeter group of `Y₄₄₃`, i.e. Mathlib's `PresentedGroup` quotient
`⟨ sᵢ | (sᵢ sⱼ)^{mᵢⱼ} = 1⟩`; the faithful analogue of the Lean 3
`coxeter_group (matrix_of_graph (coxeter_edges [4,4,3]))`. -/
abbrev Y443 : Type := Y443Matrix.Group

instance : Group Y443 := inferInstanceAs (Group Y443Matrix.Group)

/-- The Coxeter system of `Y₄₄₃`. -/
abbrev y443CoxeterSystem : CoxeterSystem Y443Matrix Y443 := Y443Matrix.toCoxeterSystem

/-- The simple reflections of `Y₄₄₃`, one for each of the twelve nodes. -/
abbrev y443Simple (i : Y443Vertex) : Y443 := Y443Matrix.simple i

@[simp] theorem y443CoxeterSystem_simple (i : Y443Vertex) :
    y443CoxeterSystem.simple i = y443Simple i := rfl

/-- Each simple reflection is an involution: the `12` relators `x^2 = 1`. -/
theorem y443Simple_mul_self (i : Y443Vertex) : y443Simple i * y443Simple i = 1 :=
  y443CoxeterSystem.simple_mul_simple_self i

/-- The `11 + 55` braid and commutator relators: `(sᵢ sⱼ)^{mᵢⱼ} = 1`, where `mᵢⱼ` is the
`(i,j)` entry of the Coxeter matrix, i.e. `3` across a bond and `2` for a non-adjacent pair. -/
theorem y443Simple_mul_simple_pow (i j : Y443Vertex) :
    (y443Simple i * y443Simple j) ^ Y443Matrix.M i j = 1 :=
  y443CoxeterSystem.simple_mul_simple_pow i j

/-- The simple reflections generate `Y₄₄₃`. -/
theorem y443_closure_range_simple : Subgroup.closure (Set.range y443Simple) = ⊤ :=
  y443CoxeterSystem.subgroup_closure_range_simple

/-- Every element of `Y₄₄₃` is a product of simple reflections. -/
theorem y443Simple_surjective :
    Function.Surjective (fun omega : List Y443Vertex => List.prod (List.map y443Simple omega)) :=
  fun w => y443CoxeterSystem.wordProd_surjective w

/-! ## The seven spider generators -/

/-- The node `a` of the spider relation: the torso, `generated_of torso` in the reference. -/
abbrev y443A : Y443 := y443Simple Y443Torso

/-- The nodes `b₁, b₂, b₃`: the first node of each arm, `generated_of $ arm i 0`. -/
abbrev y443B (i : Fin 3) : Y443 := y443Simple (Y443BNode i)

/-- The nodes `c₁, c₂, c₃`: the second node of each arm, `generated_of $ arm i 1`. -/
abbrev y443C (i : Fin 3) : Y443 := y443Simple (Y443CNode i)

/-- The spider element `(a b₁ c₁ a b₂ c₂ a b₃ c₃)^10` of the reference: quotienting `Y₄₄₃` by
it gives `M × C₂`, and quotienting further by the centre gives the Fischer--Griess monster
(task S2). -/
def y443Spider : Y443 :=
  (y443A * y443B 0 * y443C 0 * y443A * y443B 1 * y443C 1 * y443A * y443B 2 * y443C 2) ^ 10

theorem y443Spider_def :
    y443Spider = (y443A * y443B 0 * y443C 0 * y443A * y443B 1 * y443C 1 * y443A * y443B 2 *
      y443C 2) ^ 10 := rfl

/-! ## Axiom check

Not needed for the mathematics; this is the check that the file introduces no axiom beyond
Lean's three standard ones. -/

#print axioms Y443Matrix_multiset
#print axioms Y443Matrix
#print axioms y443Simple_mul_simple_pow
#print axioms y443_closure_range_simple
#print axioms y443Spider

end MM
