Fourth power of the lifted half twist equals the full twist squared

Proved

burau_sLift_pow_four

by lt9 · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

braid-groupscoxeterfull-twist

Fourth power of the lifted half twist. With $\mathrm{sLift}$ the lift of the half twist in $B_3$ , one has

\mathrm{sLift}^4 = \Delta^4 = (\sigma_0\sigma_1)^6 ,

because the amalgam dictionary gives $\mathrm{sLift}^2 = (\sigma_0\sigma_1)^3$ and squaring doubles the exponent. This is the elementary computation behind the Coxeter relation $\mathrm{liftS}^4=1$ in the reduced group.

Preamble

import Definitions.Def_burau_reduced_braid_group
import Definitions.Def_BurauFaithful_UnreducedBurau
import Theorems.Thm_BurauFaithful_braid_three_amalgam_dictionary

set_option autoImplicit false

Formal statement

theorem burau_sLift_pow_four :
    (BurauFaithful.sLift : BurauNC.B3) ^ 4 = BurauNC.Delta4 := by sorry

Source

C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups* (1964), Ch. 3.

View graph