ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Unreduced and reduced Burau matrices for three strands

Example

Assume AC (inherited through the identification of the reduced matrices with the topological representation). For $n = 3$ the unreduced Burau matrices over $Λ_{1} = Z [t^{\pm 1}]$ are $ρ_{3} (σ_{1}) = (\begin{array}{ccc} 1 - t & t & 0 \\ 1 & 0 & 0 \\ 0 & 0 & 1 \end{array}), ρ_{3} (σ_{2}) = (\begin{array}{ccc} 1 & 0 & 0 \\ 0 & 1 - t & t \\ 0 & 1 & 0 \end{array}),$ and they satisfy $ρ_{3} (σ_{1}) ρ_{3} (σ_{2}) ρ_{3} (σ_{1}) = ρ_{3} (σ_{2}) ρ_{3} (σ_{1}) ρ_{3} (σ_{2})$ . The reduced matrices in the basis $(g_{1}, g_{2}) = (t e_{1} - e_{2}, t e_{2} - e_{3})$ of the invariant-covector kernel $\ker σ$ are ${\overset{ˉ}{ρ}}_{3} (σ_{1}) = (\begin{array}{cc} - t & t \\ 0 & 1 \end{array}), {\overset{ˉ}{ρ}}_{3} (σ_{2}) = (\begin{array}{cc} 1 & 0 \\ 1 & - t \end{array}),$ and they also satisfy the braid relation; they are the matrices of the restriction of the unreduced matrices to $\ker σ$ , that is, the reduction of the unreduced matrices to the invariant-covector kernel, in agreement with clause (2) of The topological and matrix Burau representations agree.

Verification

Given: the ring $Λ_{1} = Z [t^{\pm 1}]$ with its element $t$ ; $n = 3$ ; the unreduced matrices $B_{1}, B_{2}$ of The unreduced Burau matrices; the vectors $σ = (1, t, t^{2})$ , $g_{1} = t e_{1} - e_{2}$ , $g_{2} = t e_{2} - e_{3}$ ; the reduced representation ${\overset{ˉ}{ρ}}_{3}$ of The reduced Burau representation.

[A1] $B_{i}$ is the identity outside rows and columns $i, i + 1$ and has the block $(\begin{array}{cc} 1 - t & t \\ 1 & 0 \end{array})$ there, acting on column vectors by $e_{i} \mapsto (1 - t) e_{i} + e_{i + 1}$ , $e_{i + 1} \mapsto t e_{i}$ ; matrices compose in the library order, so a word acts by the product of its matrices (The unreduced Burau matrices).

[A2] In the basis $(g_{1}, \dots, g_{n - 1})$ , $g_{i} = t e_{i} - e_{i + 1}$ $(1 \leq i \leq n - 1)$ , of $\ker σ = {x : σ (x) = 0}$ with $σ = (1, t, \dots, t^{n - 1})$ , the reduced representation acts by the three-term formulas $g_{j - 1} \mapsto g_{j - 1} + g_{j}$ , $g_{j} \mapsto - t g_{j}$ , $g_{j + 1} \mapsto t g_{j} + g_{j + 1}$ , all other $g_{i}$ fixed; for $n = 3$ this gives the two displayed $2 \times 2$ matrices (The topological and matrix Burau representations agree, clause (2); The reduced Burau representation).

[A3] $σ B_{i} = σ$ for $i = 1, 2$ , so $\ker σ$ is invariant under both $B_{1}$ and $B_{2}$ : if $σ (x) = 0$ then $σ (B_{i} x) = σ (x) = 0$ (The invariant vector and the invariant covectors of the unreduced Burau, clause (b)).

[A4] $M_{r e d}$ is free of rank $n - 1$ and is carried onto $\ker σ$ by the basis identification of the pair sequence (The reduced Burau module is free of rank n minus one, The unreduced module fits an exact sequence with the reduced module); in particular $\ker σ$ is free of rank $2$ for $n = 3$ .

[A5] $Λ_{1}$ is an integral domain in which $t \neq 0$ ; hence $a t = 0$ implies $a = 0$ . Matrices record the images of basis vectors as columns (Units, powers and the domain property of the Laurent polynomial ring (a), The Laurent polynomial ring as the principal localisation of Z[t] at t).

Proof technique: direct.

1.1A1algebra

The unreduced matrices. For $n = 3$ the block of [A1] sits in rows and columns $1, 2$ for $B_{1}$ and in rows and columns $2, 3$ for $B_{2}$ , with all other entries those of the identity: $B_{1} = (\begin{array}{ccc} 1 - t & t & 0 \\ 1 & 0 & 0 \\ 0 & 0 & 1 \end{array})$ and $B_{2} = (\begin{array}{ccc} 1 & 0 & 0 \\ 0 & 1 - t & t \\ 0 & 1 & 0 \end{array})$ , as displayed.

1.2A1algebra

The braid relation for the unreduced matrices. Direct matrix multiplication gives $B_{1} B_{2} = (\begin{array}{ccc} 1 - t & t - t^{2} & t^{2} \\ 1 & 0 & 0 \\ 0 & 1 & 0 \end{array})$ and $B_{2} B_{1} = (\begin{array}{ccc} 1 - t & t & 0 \\ 1 - t & 0 & t \\ 1 & 0 & 0 \end{array})$ ; multiplying on the right by $B_{1}$ respectively $B_{2}$ gives in both cases the matrix $(\begin{array}{ccc} 1 - t & t - t^{2} & t^{2} \\ 1 - t & t & 0 \\ 1 & 0 & 0 \end{array})$ , so $B_{1} B_{2} B_{1} = B_{2} B_{1} B_{2}$ .

1.3A1A2A3A4A5algebra

The kernel basis and the restricted action. $σ (g_{1}) = t - t = 0$ and $σ (g_{2}) = t \cdot t - t^{2} = 0$ , so $g_{1}, g_{2} \in \ker σ$ ; they are independent, because $a g_{1} + b g_{2} = 0$ reads $(a t, - a + b t, - b) = 0$ with $t \neq 0$ , so $b = 0$ , then $a = 0$ by [A5]. They also span: if $x = x_{1} e_{1} + x_{2} e_{2} + x_{3} e_{3}$ satisfies $x_{1} + t x_{2} + t^{2} x_{3} = 0$ , set $b = - x_{3}$ and $a = - x_{2} - t x_{3}$ . Then $a g_{1} + b g_{2}$ has coordinates $(a t, - a + b t, - b) = (- t x_{2} - t^{2} x_{3}, x_{2}, x_{3}) = (x_{1}, x_{2}, x_{3})$ . Thus independence and this explicit spanning prove that $(g_{1}, g_{2})$ is a $Λ_{1}$ -basis of $\ker σ$ . Since $\ker σ$ is $B_{1}$ - and $B_{2}$ -invariant by [A3], the matrices act on this basis: using the actions of [A1], $B_{1} g_{1} = t ((1 - t) e_{1} + e_{2}) - t e_{1} = - t^{2} e_{1} + t e_{2} = - t g_{1}$ and $B_{1} g_{2} = t (t e_{1}) - e_{3} = t^{2} e_{1} - e_{3} = t g_{1} + g_{2}$ ; likewise $B_{2} g_{1} = t e_{1} - ((1 - t) e_{2} + e_{3}) = t e_{1} + (t - 1) e_{2} - e_{3} = g_{1} + g_{2}$ and $B_{2} g_{2} = t ((1 - t) e_{2} + e_{3}) - t e_{2} = - t^{2} e_{2} + t e_{3} = - t g_{2}$ . Reading the two images as columns gives ${\overset{ˉ}{ρ}}_{3} (σ_{1}) = (\begin{array}{cc} - t & t \\ 0 & 1 \end{array})$ and ${\overset{ˉ}{ρ}}_{3} (σ_{2}) = (\begin{array}{cc} 1 & 0 \\ 1 & - t \end{array})$ , the displayed reduced matrices.

2.1step 1.3algebra

The braid relation for the reduced matrices. Direct multiplication gives $M_{1} M_{2} = (\begin{array}{cc} 0 & - t^{2} \\ 1 & - t \end{array})$ and $M_{2} M_{1} = (\begin{array}{cc} - t & t \\ - t & 0 \end{array})$ for $M_{1} = (\begin{array}{cc} - t & t \\ 0 & 1 \end{array})$ , $M_{2} = (\begin{array}{cc} 1 & 0 \\ 1 & - t \end{array})$ ; multiplying by $M_{1}$ respectively $M_{2}$ gives $M_{1} M_{2} M_{1} = M_{2} M_{1} M_{2} = (\begin{array}{cc} 0 & - t^{2} \\ - t & 0 \end{array})$ , so the reduced matrices satisfy the braid relation.

3.1A2step 1.3step 2.1∎

Reduction of the unreduced matrices. Step 1.3 exhibited the restricted actions of $B_{1}, B_{2}$ on the invariant kernel $\ker σ$ in the basis $(g_{1}, g_{2})$ as exactly $M_{1}, M_{2}$ , and step 2.1 verified the braid relation at both levels; hence the displayed reduced matrices are the reduction of the displayed unreduced matrices to the invariant-covector kernel, and they agree with clause (2) of [A2]. AC is inherited through the cited identification of the reduced matrices with the topological representation; the matrix computations are choice free.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Joan S. Birman and Tara E. Brendle, Braids: A Survey (background on Burau matrices, the cyclic cover and absolute homology) (standard reference, not scraped)
Vasudha Bharathram, Joan S. Birman and Tara E. Brendle, The Burau representation is faithful for n = 4, arXiv:2607.05283v1 (6 July 2026), Introduction and section 2 (printed pp. 1-5) (standard reference, not scraped)