The full twist squared is trivial in the reduced braid group

Proved

burau_q_delta4

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

braid-groupsfull-twistreduced-burau

The full twist squared is trivial in the reduced braid group. In $Q=B_3/\langle\!\langle\Delta^4\rangle\!\rangle$ , where $\Delta^4=(\sigma_0\sigma_1)^6$ , the class of $\Delta^4$ is the identity:

\overline{\Delta^4} = 1 .

This is the defining relation of the reduced group $Q$ and the reason $\Delta^4$ is the expected generator of the kernel of the reduced Burau representation.

Preamble

import Definitions.Def_burau_reduced_braid_group
import Definitions.Def_BurauFaithful_UnreducedBurau

set_option autoImplicit false

Formal statement

theorem burau_q_delta4 :
    ((BurauNC.Delta4 : BurauNC.B3) : BurauNC.Q) = 1 := by sorry

Source

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

View graph