Prove2Me

The Euclidean descent section rho of the reduced braid quotient

Definition
burau_rho

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

braid-groupscontinued-fractionsdescent-sectionsl2z

The descent section ρ:SL(2,Z)→Q\rho:\mathrm{SL}(2,\mathbb Z)\to Q of the reduced braid quotient. The definition node records the section of the quotient map q:B3→Q=B3/⟨ ⁣⟨Δ4⟩ ⁣⟩q:B_3\to Q=B_3/\langle\!\langle\Delta^4\rangle\!\rangle built from the Euclidean descent on 2×22\times2 integer matrices: the terminal value

baseQ(M)={liftS liftTM11M01=−1,liftS3 liftT−M11else,\mathtt{baseQ}(M)=\begin{cases} \mathrm{liftS}\,\mathrm{liftT}^{M_{11}} & M_{01}=-1,\\ \mathrm{liftS}^3\,\mathrm{liftT}^{-M_{11}} & \text{else,}\end{cases}

the iterated descent rhoIter\mathtt{rhoIter} with its budget, and ρ(M)=rhoIter(∣M00∣,M)\rho(M)=\mathtt{rhoIter}(|M_{00}|,M). Alongside them it records the reformulations cfEnd\mathtt{cfEnd} (the terminal matrix reached by the descent) and cfWord\mathtt{cfWord} (the Q-word accumulated from the quotient list), so that ρ(M)=baseQ(cfEnd(M))⋅cfWord(cfList(M))\rho(M)=\mathtt{baseQ}(\mathtt{cfEnd}(M))\cdot\mathtt{cfWord}(\mathtt{cfList}(M)). The two rules ρ(M⋅Tj)=ρ(M) liftTj\rho(M\cdot T^j)=\rho(M)\,\mathrm{liftT}^j and the SS-rule ρ(M⋅S)=ρ(M) liftS\rho(M\cdot S)=\rho(M)\,\mathrm{liftS} are the content of the milestone's reduction, and this node makes the section itself reusable by later platform nodes.

Definition code
import Definitions.Def_burau_cf_list
import Definitions.Def_burau_reduced_braid_group

set_option autoImplicit false

open Matrix

namespace BurauNC

noncomputable def baseQ (M : M2) : Q :=
  if M 0 1 = -1 then liftS * liftT ^ (M 1 1) else liftS ^ 3 * liftT ^ (-(M 1 1))


noncomputable def rhoIter : ℕ → M2 → Q
  | 0, M => baseQ M
  | k + 1, M =>
      if M 0 0 = 0 then baseQ M
      else rhoIter k ((M * Tm (-(M 0 1 / M 0 0))) * Sm) * liftS⁻¹ * liftT ^ (M 0 1 / M 0 0)


noncomputable def rho (M : M2) : Q := rhoIter (M 0 0).natAbs M

noncomputable def cfWord : List ℤ → Q
  | [] => 1
  | e :: l => cfWord l * (liftS⁻¹ * liftT ^ e)


noncomputable def cfEnd : M2 → M2
  | M => if h : M 0 0 = 0 then M else cfEnd ((M * Tm (-(M 0 1 / M 0 0))) * Sm)
termination_by M => (M 0 0).natAbs
decreasing_by exact euclid_decrease M h

end BurauNC
Source
Euclidean algorithm in SL(2,Z) and the reduced Burau representation; cf. C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups* (1964), Ch. 3; J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82 (1974), §3.3.

View graph