Conjugacy of the odd-order elements is read off from the permutation layer (Theorem 5)

import Mathlib
import Definitions.Def_BQC_alg
import Definitions.Def_BQC_tor

namespace BQC

/-!  Milestone 5 (Theorem 5): two elements of the braid quotient of the same
odd order at least three are conjugate in the quotient if and only if their
images are conjugate in the permutation layer. Conjugacy of elements of odd
order is read off from the permutation layer; likewise two cyclic subgroups of
the same odd order are conjugate exactly when their images are. -/
theorem conjugacy_cycle_type {n : Nat} {Q S : Type*} [Group Q] [Group S] [Fintype S]
    (W : BraidQuotient n Q S) (k : Nat) (hk : 3 ≤ k) (hodd : Odd k)
    (x y : Q) (hx : ExactOrder k x) (hy : ExactOrder k y) :
    (∃ c : Q, c * x * c⁻¹ = y) ↔
      (∃ s : S, s * W.proj x * s⁻¹ = W.proj y) := by sorry

end BQC