The cyclic subgroup generated by $\Delta^4$ dies at $t=-1$

Proved

BurauFaithful.burau_three_spec_twist_zpow

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

braid-groupsmodular-grouprepresentation-theory

This states the consequence of the relation $(\rho_3(\sigma_1\sigma_2)|_{t=-1})^6 = I_3$ for all powers demanded by the full twist, in the form needed to finish the easy direction of the three-strand faithfulness theorem (J. S. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82, §3.3, pp. 129-130).

With $B_3 = \langle\sigma_1,\sigma_2\rangle$ , $\rho_3$ the unreduced Burau representation and the specialization $\mathbb{Z}[t,t^{-1}]\to\mathbb{Z}$ , $t\mapsto-1$ , the theorem asserts that for every integer $k$ ,

\rho_3\bigl((\sigma_1\sigma_2)^{6k}\bigr)\Big|_{t=-1} = I_3 .

In other words, the whole cyclic subgroup generated by $\Delta^4=(\sigma_1\sigma_2)^6$ lies in the kernel of the specialization at $t=-1$ . This is the direction " $\beta$ a power of $\Delta^4$ $\Rightarrow$ $\beta$ dies at $t=-1$ " of the milestone burau_three_spec_kernel.

Formalization Note The specialization is LaurentPolynomial.eval₂ (Int.castRingHom ℤ) (-1 : ℤˣ), extended to matrices by Matrix.GeneralLinearGroup.map; the exponent $6k$ is an integer power in $B_3$ .

Preamble

import Definitions.Def_BurauFaithful_UnreducedBurau

set_option autoImplicit false

Formal statement

theorem BurauFaithful.burau_three_spec_twist_zpow (k : ℤ) :
    Matrix.GeneralLinearGroup.map (LaurentPolynomial.eval₂ (Int.castRingHom ℤ) (-1 : ℤˣ))
      (BurauFaithful.burauRep 3 ((BraidsLinksMCG.sigma ⟨0, by decide⟩ * BraidsLinksMCG.sigma ⟨1, by decide⟩) ^ (6 * k))) = 1 := by sorry

Source

J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, Princeton Univ. Press, 1974, Chapter 3 (Magnus representations), §3.3, Theorem 3.15, pp. 129-130 ("setting t = -1 these matrices become ... By [Coxeter-Moser, 1964, p. 85] s1 and s2 generate the homogeneous modular group M2, which has defining relations s1s2s1 = s2s1s2 and (s1s2s1)^4 = 1"); cf. V. Bharathram, J. S. Birman, T. E. Brendle, arXiv:2607.05283v2, Theorem 4.1 (Section 4).

View graph

The cyclic subgroup generated by Δ4\Delta^4Δ4 dies at t=−1t=-1t=−1

The cyclic subgroup generated by $\Delta^4$ dies at $t=-1$