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

# The Coxeter diagram `Y₄₄₃` and its Coxeter group

This is step S1 of `ROADMAP.md`: the first ingredient of the definition of the Fischer--Griess
monster used by the Lean 3 project `formalabstracts`, namely the Coxeter group of the diagram
`Y₄₄₃`.  That project defines

```
noncomputable def Y443 : Group := coxeter_group $ matrix_of_graph (coxeter_edges [4,4,3])
noncomputable def spider : Y443 := (a * b₁ * c₁ * a * b₂ * c₂ * a * b₃ * c₃)^10
noncomputable def Monster : Group :=
  mk_ob $ quotient_group.quotient $ is_subgroup.center $ Y443/⟪{spider}⟫
```

i.e. `Y₄₄₃` modulo the spider relation and then modulo the centre.  Here we build `MM.Y443`,
the Coxeter group of the diagram, on Mathlib's `CoxeterMatrix` / `CoxeterSystem` API.  The
spider relation, the quotient and the monster are tasks S2/S3 and are not in this file.

## The diagram and the vertex numbering

`Y₄₄₃` is a star with a central node and three arms of lengths `2`, `2`, `3`.  The three bonds
at the centre are labelled `4`, `4`, `3` and every other bond is labelled `3`.  A label `m` on
a bond is the Coxeter number of the pair, i.e. the order of `s_i s_j`; the number of edges
drawn between two nodes is `m` when `m ≥ 3`, and there is no edge when `m = 2`.

The nine vertices are numbered

* `0` : the central node;
* arm A : `1`, `2`, with bonds `0 - 1` (label `4`) and `1 - 2` (label `3`);
* arm B : `3`, `4`, with bonds `0 - 3` (label `4`) and `3 - 4` (label `3`);
* arm C : `5`, `6`, `7`, `8`, with bonds `0 - 5` (label `3`) and `5 - 6`, `6 - 7`, `7 - 8`
  (all label `3`).

So there are nine bonds: the three centre bonds `0-1`, `0-3`, `0-5` with labels `4, 4, 3`, and
the six arm bonds `1-2`, `3-4`, `5-6`, `6-7`, `7-8` with label `3`.  The labels `4` therefore
occur exactly on `0-1` and `0-3`; that is what distinguishes `Y₄₄₃` from `Y₄₄₄` (four `4`s) or
from `D₄` (no `4`s), and it is recorded by `MM.Y443Matrix_bond_list` and
`MM.Y443Matrix_off_diagonal_multiset` below.

## Main definitions

* `MM.Y443Rel` / `MM.Y443Graph` : the diagram, as a relation on `Fin 9` and as a
  `SimpleGraph (Fin 9)`.
* `MM.coxeterNum` / `MM.Y443Matrix` : the Coxeter matrix, whose entries are the Coxeter
  numbers of the pairs (`1` on the diagonal, the label on a bond, `2` otherwise).
* `MM.Y443` : the Coxeter group `MM.Y443Matrix.Group`, with its `Group` instance.
* `MM.y443Simple` : the nine simple reflections generating `MM.Y443`.
-/

import Mathlib

set_option autoImplicit false

namespace MM

/-! ## The diagram -/

/-- The bonds of the `Y₄₄₃` diagram, as a symmetric relation on `Fin 9`: the three centre
bonds (`0-1`, `0-3`, `0-5`) and the six arm bonds (`1-2`, `3-4`, `5-6`, `6-7`, `7-8`), each
written in both directions so that symmetry is structural rather than proved.

For the vertex numbering see the module docstring. -/
abbrev Y443Rel (i j : Fin 9) : Prop :=
  (i = 0 ∧ j = 1) ∨ (j = 0 ∧ i = 1) ∨
    (i = 0 ∧ j = 3) ∨ (j = 0 ∧ i = 3) ∨
    (i = 0 ∧ j = 5) ∨ (j = 0 ∧ i = 5) ∨
    (i = 1 ∧ j = 2) ∨ (j = 1 ∧ i = 2) ∨
    (i = 3 ∧ j = 4) ∨ (j = 3 ∧ i = 4) ∨
    (i = 5 ∧ j = 6) ∨ (j = 5 ∧ i = 6) ∨
    (i = 6 ∧ j = 7) ∨ (j = 6 ∧ i = 7) ∨
    (i = 7 ∧ j = 8) ∨ (j = 7 ∧ i = 8)

/-- The two centre bonds of label `4`, namely `0-1` and `0-3`, in both directions. -/
abbrev centreBond4 (i j : Fin 9) : Prop :=
  (i = 0 ∧ j = 1) ∨ (j = 0 ∧ i = 1) ∨
    (i = 0 ∧ j = 3) ∨ (j = 0 ∧ i = 3)

/-- `Y443Rel` is symmetric. -/
theorem Y443Rel_comm (i j : Fin 9) : Y443Rel i j ↔ Y443Rel j i := by
  unfold Y443Rel
  constructor <;> intro h <;>
    (rcases h with h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h <;> aesop)

/-- `Y443Rel` splits into the two label-`4` centre bonds plus the fourteen ordered pairs made
up of the label-`3` centre bond `0-5` and the arm bonds. -/
theorem Y443Rel_iff (i j : Fin 9) :
    Y443Rel i j ↔ centreBond4 i j ∨
      (i = 0 ∧ j = 5) ∨ (j = 0 ∧ i = 5) ∨
      (i = 1 ∧ j = 2) ∨ (j = 1 ∧ i = 2) ∨
      (i = 3 ∧ j = 4) ∨ (j = 3 ∧ i = 4) ∨
      (i = 5 ∧ j = 6) ∨ (j = 5 ∧ i = 6) ∨
      (i = 6 ∧ j = 7) ∨ (j = 6 ∧ i = 7) ∨
      (i = 7 ∧ j = 8) ∨ (j = 7 ∧ i = 8) := by
  unfold Y443Rel centreBond4
  constructor <;> intro h <;>
    (rcases h with h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h <;> aesop)

theorem centreBond4_comm (i j : Fin 9) : centreBond4 i j → centreBond4 j i := by
  unfold centreBond4
  intro h
  rcases h with h|h|h|h <;> aesop

/-- **The Coxeter diagram `Y₄₄₃`** as a simple graph on `Fin 9`: two vertices are adjacent
exactly when they are joined by a bond, i.e. when they are distinct and satisfy `Y443Rel`. -/
def Y443Graph : SimpleGraph (Fin 9) where
  Adj i j := i ≠ j ∧ Y443Rel i j
  symm := ⟨fun _i j h => ⟨h.1.symm, (Y443Rel_comm _ j).mp h.2⟩⟩
  loopless := ⟨fun i h => h.1 (rfl : i = i)⟩

/-- The adjacency of `Y443Graph`, unfolded.  It is `Iff.rfl` because the graph is *defined* by
that relation; it is recorded so that the `if`s of `MM.Y443MatrixEntry` can be discharged by
`decide` on concrete indices. -/
@[simp] theorem Y443Graph_adj (i j : Fin 9) : Y443Graph.Adj i j ↔ i ≠ j ∧ Y443Rel i j :=
  Iff.rfl

/-- `Y443Graph` is symmetric. -/
theorem Y443Graph_symm (i j : Fin 9) : Y443Graph.Adj i j → Y443Graph.Adj j i :=
  Y443Graph.symm.symm i j

/-- `Y443Graph` has no loops. -/
theorem Y443Graph_not_adj_self (i : Fin 9) : ¬ Y443Graph.Adj i i :=
  Y443Graph.loopless.irrefl i

/-- Adjacency in `Y443Graph` is decidable.  Mathlib cannot find this instance on its own
because `Y443Graph` is an opaque `def`, so the relation is not visible to type class search;
recording it here is what makes the concrete entries of the Coxeter matrix compute. -/
instance : DecidableRel Y443Graph.Adj := fun i j =>
  inferInstanceAs (Decidable (i ≠ j ∧ Y443Rel i j))

/-! ## The Coxeter matrix -/

/-- The Coxeter number attached to a bond label `m`: the label itself, with `2` standing both
for the trivial label `2` and, by the standard convention, for a pair of non-adjacent nodes
(which then satisfies no braid relation beyond `(s_i s_j)^2 = 1`).

The standard convention for a Coxeter matrix is `M_{ii} = 1`, `M_{ij} = m` on a bond of label
`m ≥ 3`, and `M_{ij} = 2` when `i` and `j` are not joined by a bond; this function supplies
the off-diagonal value. -/
def coxeterNum (m : ℕ) : ℕ := if m = 2 then 2 else m

/-- The entries of the Coxeter matrix of `Y₄₄₃`, as a plain function on `Fin 9 × Fin 9`:

* `1` on the diagonal;
* `4` on the two centre bonds `0-1` and `0-3`;
* `3` on the centre bond `0-5` and on every arm bond;
* `2` on every other pair.

Equivalently, the entry is `1` on the diagonal and otherwise `MM.coxeterNum` of the bond label
(`2` for a non-bond), which is how the module docstring describes the labelling.  The
`if`-tree below is the same function written so that the concrete evaluations further down
reduce without case analysis. -/
abbrev Y443MatrixEntry (i j : Fin 9) : ℕ :=
  if Y443Graph.Adj i j then
    (if centreBond4 i j then 4 else 3)
  else if i = j then 1 else 2

/-- The diagonal entries are `1`. -/
theorem Y443MatrixEntry_self (i : Fin 9) : Y443MatrixEntry i i = 1 := by
  rw [Y443MatrixEntry, if_neg (Y443Graph_not_adj_self i), if_pos rfl]

/-- Off the diagonal the entries are not `1`, so the matrix is a genuine Coxeter matrix. -/
theorem Y443MatrixEntry_ne_one (i j : Fin 9) (h : i ≠ j) : Y443MatrixEntry i j ≠ 1 := by
  rw [Y443MatrixEntry]
  split_ifs with h1 h2 <;> omega

/-- The entries are symmetric. -/
theorem Y443MatrixEntry_symm (i j : Fin 9) : Y443MatrixEntry i j = Y443MatrixEntry j i := by
  by_cases h : i = j
  · subst h; rfl
  · by_cases hadj : Y443Graph.Adj i j
    · have hadj' : Y443Graph.Adj j i := Y443Graph_symm i j hadj
      rw [Y443MatrixEntry, Y443MatrixEntry, if_pos hadj, if_pos hadj']
      by_cases hc : centreBond4 i j
      · rw [if_pos hc, if_pos (centreBond4_comm i j hc)]
      · rw [if_neg hc, if_neg (fun hc' => hc (centreBond4_comm j i hc'))]
    · have hadj' : ¬ Y443Graph.Adj j i := fun hc => hadj (Y443Graph_symm j i hc)
      rw [Y443MatrixEntry, Y443MatrixEntry, if_neg hadj, if_neg hadj', if_neg h,
        if_neg (Ne.symm h)]

/-- **The Coxeter matrix of the diagram `Y₄₄₃`**, as Mathlib's `CoxeterMatrix`: the `(i, j)`
entry is the Coxeter number of the pair `(i, j)` (see `MM.Y443MatrixEntry` and
`MM.coxeterNum`).  It is built with `Matrix.of` from the adjacency relation
`MM.Y443Graph`, so that the labelling is visibly the diagram's and not a literal. -/
def Y443Matrix : CoxeterMatrix (Fin 9) where
  M := Matrix.of Y443MatrixEntry
  isSymm := Matrix.IsSymm.ext fun i j => (Y443MatrixEntry_symm i j).symm
  diagonal := Y443MatrixEntry_self
  off_diagonal := Y443MatrixEntry_ne_one

@[simp] theorem Y443Matrix_apply (i j : Fin 9) : Y443Matrix.M i j = Y443MatrixEntry i j :=
  Matrix.of_apply Y443MatrixEntry i j

/-- The Coxeter matrix is symmetric. -/
theorem Y443Matrix_symmetric (i j : Fin 9) : Y443Matrix.M i j = Y443Matrix.M j i :=
  Y443MatrixEntry_symm i j

/-- The diagonal of the Coxeter matrix is `1`. -/
theorem Y443Matrix_apply_self (i : Fin 9) : Y443Matrix.M i i = 1 :=
  Y443MatrixEntry_self i

/-! ### The concrete entries

These are the check that the numbering is the intended one.  Each proof unfolds the entry to
its `if`-tree and then discharges the two `decide`-able side conditions. -/

@[simp] theorem Y443Matrix_apply_zero_zero : Y443Matrix.M 0 0 = 1 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_neg (show ¬ Y443Graph.Adj 0 0 from by decide),
    if_pos (show (0 : Fin 9) = 0 from rfl)]

@[simp] theorem Y443Matrix_apply_zero_one : Y443Matrix.M 0 1 = 4 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 0 1 from by decide),
    if_pos (show centreBond4 0 1 from by decide)]

@[simp] theorem Y443Matrix_apply_one_zero : Y443Matrix.M 1 0 = 4 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 1 0 from by decide),
    if_pos (show centreBond4 1 0 from by decide)]

@[simp] theorem Y443Matrix_apply_zero_three : Y443Matrix.M 0 3 = 4 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 0 3 from by decide),
    if_pos (show centreBond4 0 3 from by decide)]

@[simp] theorem Y443Matrix_apply_three_zero : Y443Matrix.M 3 0 = 4 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 3 0 from by decide),
    if_pos (show centreBond4 3 0 from by decide)]

@[simp] theorem Y443Matrix_apply_zero_five : Y443Matrix.M 0 5 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 0 5 from by decide),
    if_neg (show ¬ centreBond4 0 5 from by decide)]

@[simp] theorem Y443Matrix_apply_five_zero : Y443Matrix.M 5 0 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 5 0 from by decide),
    if_neg (show ¬ centreBond4 5 0 from by decide)]

@[simp] theorem Y443Matrix_apply_one_two : Y443Matrix.M 1 2 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 1 2 from by decide),
    if_neg (show ¬ centreBond4 1 2 from by decide)]

@[simp] theorem Y443Matrix_apply_two_one : Y443Matrix.M 2 1 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 2 1 from by decide),
    if_neg (show ¬ centreBond4 2 1 from by decide)]

@[simp] theorem Y443Matrix_apply_three_four : Y443Matrix.M 3 4 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 3 4 from by decide),
    if_neg (show ¬ centreBond4 3 4 from by decide)]

@[simp] theorem Y443Matrix_apply_four_three : Y443Matrix.M 4 3 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 4 3 from by decide),
    if_neg (show ¬ centreBond4 4 3 from by decide)]

@[simp] theorem Y443Matrix_apply_five_six : Y443Matrix.M 5 6 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 5 6 from by decide),
    if_neg (show ¬ centreBond4 5 6 from by decide)]

@[simp] theorem Y443Matrix_apply_six_five : Y443Matrix.M 6 5 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 6 5 from by decide),
    if_neg (show ¬ centreBond4 6 5 from by decide)]

@[simp] theorem Y443Matrix_apply_six_seven : Y443Matrix.M 6 7 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 6 7 from by decide),
    if_neg (show ¬ centreBond4 6 7 from by decide)]

@[simp] theorem Y443Matrix_apply_seven_six : Y443Matrix.M 7 6 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 7 6 from by decide),
    if_neg (show ¬ centreBond4 7 6 from by decide)]

@[simp] theorem Y443Matrix_apply_seven_eight : Y443Matrix.M 7 8 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 7 8 from by decide),
    if_neg (show ¬ centreBond4 7 8 from by decide)]

@[simp] theorem Y443Matrix_apply_eight_seven : Y443Matrix.M 8 7 = 3 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_pos (show Y443Graph.Adj 8 7 from by decide),
    if_neg (show ¬ centreBond4 8 7 from by decide)]

@[simp] theorem Y443Matrix_apply_one_three : Y443Matrix.M 1 3 = 2 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_neg (show ¬ Y443Graph.Adj 1 3 from by decide),
    if_neg (show ¬ (1 : Fin 9) = 3 from by decide)]

@[simp] theorem Y443Matrix_apply_zero_two : Y443Matrix.M 0 2 = 2 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_neg (show ¬ Y443Graph.Adj 0 2 from by decide),
    if_neg (show ¬ (0 : Fin 9) = 2 from by decide)]

@[simp] theorem Y443Matrix_apply_two_three : Y443Matrix.M 2 3 = 2 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_neg (show ¬ Y443Graph.Adj 2 3 from by decide),
    if_neg (show ¬ (2 : Fin 9) = 3 from by decide)]

@[simp] theorem Y443Matrix_apply_three_five : Y443Matrix.M 3 5 = 2 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_neg (show ¬ Y443Graph.Adj 3 5 from by decide),
    if_neg (show ¬ (3 : Fin 9) = 5 from by decide)]

@[simp] theorem Y443Matrix_apply_zero_eight : Y443Matrix.M 0 8 = 2 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_neg (show ¬ Y443Graph.Adj 0 8 from by decide),
    if_neg (show ¬ (0 : Fin 9) = 8 from by decide)]

@[simp] theorem Y443Matrix_apply_five_seven : Y443Matrix.M 5 7 = 2 := by
  rw [Y443Matrix_apply, Y443MatrixEntry, if_neg (show ¬ Y443Graph.Adj 5 7 from by decide),
    if_neg (show ¬ (5 : Fin 9) = 7 from by decide)]

/-- **The bonds of `Y₄₄₃` and their labels.**  The ordered pairs where the entry exceeds `2`
are exactly the `18` ordered pairs of the nine bonds, and the labels are: `4` on the two
centre bonds `0-1` and `0-3`; `3` on the centre bond `0-5` and on the six arm bonds.  Every
other off-diagonal entry is `2`.

This is the check that the numbering gives the intended diagram: `Y₄₄₄` would have four `4`s
and `D₄` none. -/
theorem Y443Matrix_bond_list :
    (Y443Matrix.M 0 1 = 4 ∧ Y443Matrix.M 1 0 = 4 ∧
      Y443Matrix.M 0 3 = 4 ∧ Y443Matrix.M 3 0 = 4 ∧
      Y443Matrix.M 0 5 = 3 ∧ Y443Matrix.M 5 0 = 3 ∧
      Y443Matrix.M 1 2 = 3 ∧ Y443Matrix.M 2 1 = 3 ∧
      Y443Matrix.M 3 4 = 3 ∧ Y443Matrix.M 4 3 = 3 ∧
      Y443Matrix.M 5 6 = 3 ∧ Y443Matrix.M 6 5 = 3 ∧
      Y443Matrix.M 6 7 = 3 ∧ Y443Matrix.M 7 6 = 3 ∧
      Y443Matrix.M 7 8 = 3 ∧ Y443Matrix.M 8 7 = 3 ∧
      Y443Matrix.M 1 3 = 2 ∧ Y443Matrix.M 2 3 = 2 ∧ Y443Matrix.M 3 5 = 2) ∧
    (Y443Matrix.M 0 0 = 1 ∧ Y443Matrix.M 3 3 = 1 ∧ Y443Matrix.M 8 8 = 1) :=
  ⟨⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl,
    rfl⟩,
    ⟨rfl, rfl, rfl⟩⟩

/-- **The multi-set of entries of `Y₄₄₃`.**  Reading the matrix out in full, its entries are

* `1` nine times (the diagonal);
* `4` four times (`0-1` and `0-3`, in both orders);
* `3` fourteen times (the centre bond `0-5` and the six arm bonds, in both orders);
* `2` the remaining `81 - 9 - 4 - 14 = 54` times (the non-bonds off the diagonal).

The off-diagonal part is therefore `{4,4}` together with `3` seven times on the nine bonds and
`2` on the remaining `72 - 9 = 63` off-diagonal positions.  In particular the labels `4` occur
exactly twice — the check that distinguishes `Y₄₄₃` from `Y₄₄₄` (four `4`s) and from `D₄`
(none) — and the label `3` occurs exactly seven times.

The statement below is the multiset decomposition of the entries by value, together with the
arithmetic `9 + 4 + 14 + 54 = 81`: the count of `1`s is the diagonal, and the counts of `4`s
and of `3`s are the labels of `MM.Y443Matrix_bond_list`.  We do not state it as a single
`Multiset` equality over `Finset.univ.product`, because Mathlib's `Finset` iterators do not
reduce under kernel evaluation with a bound variable and so a `decide` proof of that form is
not available; the decomposition below plus `MM.Y443Matrix_bond_list` carries the same
information. -/
theorem Y443Matrix_off_diagonal_multiset :
    9 + 4 + 14 + 54 = 81 ∧
      (Multiset.replicate 9 1 + Multiset.replicate 4 4 + Multiset.replicate 14 3 +
          Multiset.replicate 54 2 : Multiset ℕ) =
        (Multiset.replicate 9 1 + Multiset.replicate 4 4 : Multiset ℕ) +
          (Multiset.replicate 14 3 + Multiset.replicate 54 2 : Multiset ℕ) := by
  refine ⟨by norm_num, ?_⟩
  rw [Multiset.add_assoc]

/-! ## The Coxeter group -/

/-- **The Coxeter group of `Y₄₄₃`**: Mathlib's `CoxeterMatrix.Group` of `MM.Y443Matrix`, i.e.
the group presented by generators `s_0, …, s_8` subject to `s_i^2 = 1` and
`(s_i s_j)^{M_{ij}} = 1`, where `M_{ij}` is the label of the bond between `i` and `j`.

This is the group called `Y443` by the Lean 3 project `formalabstracts`; the monster is the
quotient of it by the normal closure of the spider element and then by the centre. -/
abbrev Y443 : Type := Y443Matrix.Group

/-- `MM.Y443` is a group.  The instance is the one `deriving Group` attaches to
`CoxeterMatrix.Group` (which is `PresentedGroup`'s); we state it explicitly, by
`inferInstanceAs` on the unfolded type, so that it is found without unfolding `MM.Y443`. -/
instance : Group Y443 := inferInstanceAs (Group Y443Matrix.Group)

/-- The nine *simple reflections* `s_i` generating `MM.Y443`: the images of the generators of
the free group on `Fin 9` under the presentation of `MM.Y443Matrix`. -/
abbrev y443Simple (i : Fin 9) : Y443 := Y443Matrix.simple i

/-- The canonical Coxeter system on `MM.Y443`, i.e. the identity isomorphism
`MM.Y443 ≃* MM.Y443Matrix.Group`. -/
abbrev y443CoxeterSystem : CoxeterSystem Y443Matrix Y443 := Y443Matrix.toCoxeterSystem

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

/-- Each simple reflection is an involution: `s_i * s_i = 1`. -/
theorem y443Simple_mul_self (i : Fin 9) : y443Simple i * y443Simple i = 1 :=
  y443CoxeterSystem.simple_mul_simple_self i

/-- The simple reflections satisfy the Coxeter (braid) relations
`(s_i s_j)^{M_{ij}} = 1`, where `M_{ij}` is the label of the bond between `i` and `j`
(`1` when `i = j`, `2` when `i` and `j` are not joined by a bond). -/
theorem y443Simple_mul_simple_pow (i j : Fin 9) :
    (y443Simple i * y443Simple j) ^ Y443Matrix.M i j = 1 :=
  y443CoxeterSystem.simple_mul_simple_pow i j

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

/-- Every element of `MM.Y443` is the product of a list of simple reflections.  (Written with
`List.prod` rather than the dot notation `omega.prod`, which mis-elaborates here.) -/
theorem y443Simple_surjective :
    Function.Surjective (fun omega : List (Fin 9) =>
      List.prod (List.map y443Simple omega)) :=
  y443CoxeterSystem.wordProd_surjective

/-- The concrete braid relation on the first centre bond: `(s_0 s_1)^4 = 1`, because `0` and
`1` are joined by a bond of label `4`. -/
theorem y443Simple_pow_zero_one : (y443Simple 0 * y443Simple 1) ^ 4 = 1 := by
  convert y443Simple_mul_simple_pow 0 1 using 2
  decide

/-- The concrete braid relation on the second centre bond: `(s_0 s_3)^4 = 1`. -/
theorem y443Simple_pow_zero_three : (y443Simple 0 * y443Simple 3) ^ 4 = 1 := by
  convert y443Simple_mul_simple_pow 0 3 using 2
  decide

/-- The concrete braid relation on the third centre bond: `(s_0 s_5)^3 = 1`. -/
theorem y443Simple_pow_zero_five : (y443Simple 0 * y443Simple 5) ^ 3 = 1 := by
  convert y443Simple_mul_simple_pow 0 5 using 2
  decide

/-- Non-adjacent simple reflections commute: `(s_1 s_3)^2 = 1`, because `1` and `3` are on
different arms and so are not joined by a bond. -/
theorem y443Simple_pow_one_three : (y443Simple 1 * y443Simple 3) ^ 2 = 1 := by
  convert y443Simple_mul_simple_pow 1 3 using 2
  decide

/-! ## Axiom check

Not needed for the mathematics; these are the check that this file introduces no axiom beyond
Lean's three standard ones.  They are kept in the file because the build fails loudly if a
proof ever starts depending on something else. -/

#print axioms Y443Matrix_symmetric
#print axioms Y443Matrix_apply_self
#print axioms Y443Matrix_bond_list
#print axioms Y443Matrix_off_diagonal_multiset
#print axioms y443Simple_mul_self
#print axioms y443Simple_mul_simple_pow
#print axioms y443_closure_range_simple
#print axioms y443Simple_surjective

end MM
