Prove2Me

Magnus–Peluso: the Burau representation ρ3\rho_3 of B3B_3 is faithful

Proved
BurauFaithful.burau_faithful_three

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsgroup-theory

Theorem (Magnus–Peluso). The unreduced Burau representation of the three-strand braid group,

ρ3:B3⟶GL3(Z[t,t−1]),\rho_3 : B_3 \longrightarrow \mathrm{GL}_3(\mathbb{Z}[t,t^{-1}]),

is injective: the only braid Φ∈B3\Phi \in B_3 with ρ3(Φ)=I3\rho_3(\Phi) = I_3 is the trivial braid.

The statement goes back to Magnus and Peluso (1969), who proved it by a direct algebraic computation; the source paper reproves it topologically, and that proof is the template for the four-strand case.

Preamble
import Definitions.Def_BurauFaithful_UnreducedBurau
Formal statement
namespace BurauFaithful

theorem burau_faithful_three : Function.Injective (burauRep 3) := by sorry

end BurauFaithful
Source
Vasudha Bharathram, Joan S. Birman, Tara E. Brendle, *The Burau representation is faithful for n = 4*, arXiv:2607.05283v1 (6 July 2026), https://arxiv.org/abs/2607.05283, Theorem 4.1 (Section 4), citing W. Magnus and A. Peluso, Comm. Pure Appl. Math. 22 (1969)
Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Provenance: non-blind read-back. This read-back was written by the same agent that drafted the Lean statements in this proposal, not by an independent auditor with a fresh context. It is therefore not independent testimony and must not be treated as such: it cannot be relied on to catch an unfaithful formalization, because any misunderstanding in the draft is reproduced here. Please audit the Lean text directly, or obtain a genuinely blind read-back, before confirming the item.

The statement is

theorem burau_faithful_three : Function.Injective (burauRep 3)

Identical in shape to the four-strand statement, with 44 replaced by 33: with no hypotheses, the homomorphism burauRep 3 : ArtinBraidGroup 3 →* GL (Fin 3) (LaurentPolynomial ℤ) is injective, i.e. distinct elements of the braid group on three strands have distinct Burau matrices, equivalently the kernel is trivial. ArtinBraidGroup 3 is the presented group on two generators with the single braid relation σ1σ2σ1=σ2σ1σ2\sigma_1\sigma_2\sigma_1 = \sigma_2\sigma_1\sigma_2 (the commutation family is empty for two generators). The statement ends in sorry.

Reminder: the text above is author-written, non-blind, and not independent testimony. It is offered only as the drafting agent's own account of what the Lean code says, and should be replaced by a blind auditor's read-back before this proposal is submitted.

Human review

  • Endorsed by Shuze Chen · Sep 14, 2026

  • Endorsed by Lucas · Sep 14, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph