Last mile: normal closure of the central generator Delta^4 is an explicit power

Proved

BurauFaithful.spec_reduced_kernel_last_mile

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

braid-groupsburaumodular-group

Last mile of the kernel computation. Let $\beta\in B_3$ be a braid lying in the normal closure of the kernel generator $\Delta^4=(\sigma_1\sigma_2)^6$ . Then $\beta$ is an explicit power of that generator:

\beta\in\bigl\langle\!\bigl\langle (\sigma_1\sigma_2)^6\bigr\rangle\!\bigr\rangle\ \Longrightarrow\ \exists\,k\in\mathbb Z,\quad \beta=(\sigma_1\sigma_2)^{6k}.

Indeed $\Delta^4$ is central in $B_3$ (it is $(\Delta^2)^2$ with $\Delta^2=(\sigma_1\sigma_2)^3$ the square of the Garside element, a generator of the centre), and the normal closure of a central element coincides with the cyclic subgroup it generates. Rewriting membership in a cyclic subgroup as an explicit power finishes the argument.

This is the exact final step of the target statement that the kernel of the specialization at $t=-1$ of the reduced Burau representation is generated by $\Delta^4$ (Birman, Braids, Links, and Mapping Class Groups, Ann. of Math. Studies 82, §3.3, pp. 129–130): the remaining input, produced on the other side of the argument, is that a braid killed by the specialization lies in that normal closure.

Formalization Note Uses the Proved theorem that $\Delta^2$ is central, the accepted lemma normalClosure_singleton_center, Subgroup.mem_closure_singleton to convert subgroup membership into a power, and zpow_mul to identify $((\sigma_1\sigma_2)^6)^k$ with $(\sigma_1\sigma_2)^{6k}$ .

Preamble

/-
`BurauFaithful.spec_reduced_kernel_last_mile`: the final algebraic step of
`BurauFaithful.spec_reduced_kernel_le`.

That node asks: if `β ∈ B₃` is killed by the specialization at `t = -1`, then `β = (σ₀σ₁)^{6k}` for
some integer `k`. Everything needed for the *last mile* is:

* the Proved platform node `BurauFaithful.braid_three_fullTwist_central` — `Δ² = (σ₀σ₁)³` is central
  in `B₃`, hence so is `Δ⁴ = (σ₀σ₁)⁶ = (Δ²)²` (the centre is a subgroup);
* the accepted node `BurauFaithful.normalClosure_singleton_center` — the normal closure of a
  **central** element `g` is just its cyclic subgroup `⟨g⟩`.

Hence, once the injectivity side of the story has produced `β ∈ normalClosure {(σ₀σ₁)⁶}`, this lemma
rewrites that membership as an explicit power:
`β ∈ ⟨(σ₀σ₁)⁶⟩`, i.e. `β = ((σ₀σ₁)⁶)^k = (σ₀σ₁)^{6k}` for some `k ∈ ℤ`.

NOTE (platform rule): this file imports only **Proved/Accepted** nodes. Importing an Open node into a
problem statement is rejected by the platform ("Imported platform theorems must be Proved at
submission time"); that is also why the centrality of `(σ₀σ₁)⁶` is derived here from the Proved `Δ²`
node rather than imported from `BurauFaithful.braid_three_garside_sixth_central` (itself still Open).
-/
import Theorems.Thm_BurauFaithful_normalClosure_singleton_center
import Theorems.Thm_BurauFaithful_braid_three_fullTwist_central

set_option autoImplicit false

Formal statement

theorem BurauFaithful.spec_reduced_kernel_last_mile (β : BraidsLinksMCG.ArtinBraidGroup 3)
    (hβ : β ∈ Subgroup.normalClosure
      ({(BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩ *
        BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩) ^ 6} :
          Set (BraidsLinksMCG.ArtinBraidGroup 3))) :
    ∃ k : ℤ, β = (BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩ *
      BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩) ^ (6 * k) := by sorry

Source

J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, Princeton Univ. Press, 1974, §3.3, pp. 129-130.

View graph