The regular coverings of the lattice corrections (Propositions 3.5 and 3.10)

import Mathlib
import Definitions.Def_CTB_alg
import Definitions.Def_CTB_tor

namespace CTB

/-!  Milestone 6 (Propositions 3.5 and 3.10): the regular coverings of
the lattice corrections. For every n of at least four strings there is a
pair of nested subgroups whose quotient is of order two, given by a
character of the braid quotient with the smaller subgroup as its kernel
on the larger one - the regular double covering of the G4 lattice
correction; and there is a second pair of nested subgroups with the
smaller subgroup cut out by three simultaneous characters, jointly
surjective on triples of signs - the regular eight-sheeted covering of
the G6 lattice correction, with deck transformation group the order
eight elementary two-group. -/
theorem covering_double {n : ℕ} {Q : Type*} [Group Q]
    (W : CrystallographicBraidWorld n Q) (hn : 4 ≤ n) :
    (∃ (T1 T2 : Subgroup Q) (chi : Q →* Multiplicative (ZMod 2)),
        T1 ≤ T2 ∧
        (∀ g ∈ T2, ∀ k ∈ T1, g * k * g⁻¹ ∈ T1) ∧
        (∀ x ∈ T2, chi x = 1 ↔ x ∈ T1) ∧
        (∀ y : Multiplicative (ZMod 2), ∃ x ∈ T2, chi x = y)) ∧
    (∃ (T3 T4 : Subgroup Q) (chis : Fin 3 → (Q →* Multiplicative (ZMod 2))),
        T3 ≤ T4 ∧
        (∀ g ∈ T4, ∀ k ∈ T3, g * k * g⁻¹ ∈ T3) ∧
        (∀ x ∈ T4, (∀ j, chis j x = 1) ↔ x ∈ T3) ∧
        (∀ ys : Fin 3 → Multiplicative (ZMod 2), ∃ x ∈ T4, ∀ j, chis j x = ys j)) := by sorry

end CTB