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.

Specializing Burau at t = 1 recovers permutation data

Example

Let $n \geq 2$ . At $t = 1$ the unreduced Burau matrices specialize to permutation matrices: the block of The unreduced Burau matrices becomes $(\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ , so $ρ_{n}^{m a t} (1) (σ_{i})$ is the permutation matrix of the transposition $(i i + 1)$ and the specialization factors through the surjection $π_{n} : B_{n} \to S_{n}$ of The braid group surjects onto the symmetric group, giving the natural permutation representation of $S_{n}$ on $Z^{n}$ . Under this specialization the invariant vector $v = (1, \dots, 1)^{T}$ spans a trivial submodule, and the short exact sequence $0 \to \ker σ \to Λ_{1}^{n} \overset{(t - 1) σ}{\to} (t - 1) Λ_{1} \to 0$ (the image part of the exact sequence of The unreduced module fits an exact sequence with the reduced module, used here only through its choice-free exactness and connecting-map clauses; its $B_{n}$ -equivariance clause and the AC inherited there are not needed, and $σ$ is the invariant covector) specializes at $t = 1$ to $0 \to {x \in Z^{n} : \sum_{i} x_{i} = 0} \to Z^{n} \overset{\sum}{\to} Z \to 0.$ Over $Q$ this splits as $Q^{n} = Q v \oplus {x : \sum_{i} x_{i} = 0}$ , with $Q v$ trivial and the second summand the reduced permutation representation of $S_{n}$ ; over $Z$ the sum $Z v + {x : \sum_{i} x_{i} = 0}$ is only the proper sublattice ${x : \sum_{i} x_{i} \equiv 0 (m o d n)}$ , so the rational splitting is not an integral direct sum. The case $n = 2$ gives the sign representation on the reduced summand.

Verification

Given: $n \geq 2$ , the ring $Λ_{1} = Z [t^{\pm 1}]$ with its augmentation $ε : Λ_{1} \to Z$ , $t \mapsto 1$ (kernel $(t - 1)$ ), the matrices $B_{1}, \dots, B_{n - 1}$ and the homomorphism $ρ_{n}^{m a t} : B_{n} \to {GL}_{n} (Λ_{1})$ , the vectors $v = (1, \dots, 1)^{T}$ and $σ = (1, t, \dots, t^{n - 1})$ .

[A1] The matrices $B_{i}$ , the homomorphism $ρ_{n}^{m a t}$ , the invariant vector $v$ and covector $σ$ are as in The unreduced Burau matrices, The unreduced Burau matrices satisfy the Artin relations and The invariant vector and the invariant covectors of the unreduced Burau.

[A2] The augmentation is a unital ring homomorphism with $ε (t^{k}) = 1$ and $\ker ε = (t - 1)$ ; the exact sequence $0 \to \ker σ \to Λ_{1}^{n} \overset{(t - 1) σ}{\to} (t - 1) Λ_{1} \to 0$ is the image part of The unreduced module fits an exact sequence with the reduced module, with $σ (x) = \sum_{i} t^{i - 1} x_{i}$ (The Laurent polynomial ring as the principal localisation of Z[t] at t, Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

[A3] The braid group surjects onto the symmetric group by $σ_{i} \mapsto (i i + 1)$ , and $S_{n}$ has the Coxeter presentation with generators $s_{i} = (i i + 1)$ and relations $s_{i}^{2} = 1$ , $s_{i} s_{i + 1} s_{i} = s_{i + 1} s_{i} s_{i + 1}$ , $s_{i} s_{j} = s_{j} s_{i}$ for $∣ i - j ∣ > 1$ ; von Dyck's theorem attaches a homomorphism to any generator assignment satisfying the relators (The braid group surjects onto the symmetric group, The symmetric group has the Coxeter presentation, Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group, The finite symmetric group $S_{n}$ , one-line notation, and cycle notation).

[A4] Matrix arithmetic is entrywise over the commutative ring $Λ_{1}$ or $Z$ , and the matrix of a linear map in a fixed basis records the images of the basis vectors as columns (Invertible square matrices and similarity over a commutative ring).

Proof technique: direct.

1.1A1A2A4algebra

Specialization of the generators. Applying the augmentation $ε$ entrywise to $ρ_{n}^{m a t}$ gives the homomorphism $Θ : = ε_{*} \circ ρ_{n}^{m a t} : B_{n} \to {GL}_{n} (Z)$ , since $ε$ is a unital ring homomorphism [A2]. On the generator, $ε (1 - t) = 0$ and $ε (t) = 1$ , so the block of $B_{i}$ becomes $(\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ and the identity entries stay $1$ ; hence $Θ (σ_{i}) = E_{i}$ , the permutation matrix of the transposition $(i i + 1)$ , namely the matrix swapping the $i$ -th and $(i + 1)$ -st coordinates.

2.1A3step 1.1

Factorization through $π_{n}$ . The matrices $E_{i}$ satisfy $E_{i}^{2} = I$ , $E_{i} E_{i + 1} E_{i} = E_{i + 1} E_{i} E_{i + 1}$ and $E_{i} E_{j} = E_{j} E_{i}$ for $∣ i - j ∣ > 1$ , because they are the matrices of the corresponding permutations of the coordinate basis. By the Coxeter presentation and von Dyck [A3] there is a homomorphism $Φ : S_{n} \to {GL}_{n} (Z)$ with $Φ (s_{i}) = E_{i}$ , the natural permutation representation on $Z^{n}$ ; then $Φ \circ π_{n}$ and $Θ$ are homomorphisms $B_{n} \to {GL}_{n} (Z)$ agreeing on the generators, hence equal. So the specialization factors through the surjection $π_{n}$ and is exactly the permutation representation.

3.1A1A2step 2.1algebra

Invariant line and the specialized sequence. Every permutation matrix fixes $v$ , so $Z v$ is a trivial submodule. Put $N = \ker σ$ . Since $σ (e_{1}) = 1$ , every $x \in Λ_{1}^{n}$ has the unique decomposition $x = (x - σ (x) e_{1}) + σ (x) e_{1}$ , giving $Λ_{1}^{n} = N \oplus Λ_{1} e_{1}$ . Consequently $N \cap (t - 1) Λ_{1}^{n} = (t - 1) N$ , and $N / (t - 1) N$ injects into $Z^{n}$ . Its image is the sum-zero lattice: one inclusion follows by evaluating $σ (x) = 0$ at $t = 1$ ; conversely, if $\overset{ˉ}{x} \in Z^{n}$ has sum zero, take its constant-coordinate lift $x$ and replace it by $x - σ (x) e_{1}$ , which is in $N$ and still reduces to $\overset{ˉ}{x}$ . Multiplication $a \mapsto (t - 1) a$ is an isomorphism $Λ_{1} \to (t - 1) Λ_{1}$ , because $Λ_{1}$ is a domain and $t - 1 \neq 0$ by Units, powers and the domain property of the Laurent polynomial ring. Thus the specialized target is $(t - 1) Λ_{1} / (t - 1)^{2} Λ_{1} ≅ Z$ , where the class of $(t - 1) a$ maps to $ε (a)$ ; the map $(t - 1) σ$ becomes the sum functional. This proves the asserted specialized exact sequence, without assuming that an arbitrary specialization preserves injectivity.

4.1step 3.1algebra

Rational splitting and integral failure. Over $Q$ every $x \in Q^{n}$ is $(\sum_{i} x_{i} / n) v + (x - (\sum_{i} x_{i} / n) v)$ with the second summand of sum zero, and $Q v \cap {x : \sum_{i} x_{i} = 0} = 0$ because $n a v = 0$ forces $a = 0$ ; both summands are preserved by the permutation action, and $Q v$ is trivial, so the second summand is the reduced permutation representation. Over $Z$ , an element of $Z v + {x : \sum_{i} x_{i} = 0}$ has coordinate sum $n a$ for some $a \in Z$ , so the sum is contained in ${x : \sum_{i} x_{i} \equiv 0 m o d n}$ , and conversely $x$ with $n ∣ \sum_{i} x_{i}$ is $a v + y$ with $a = (\sum_{i} x_{i}) / n$ and $y$ of sum zero; the containment is proper because $(1, 0, \dots, 0)$ has sum $1$ and $n \geq 2$ . Hence the rational splitting is not an integral direct sum.

5.1step 4.1∎

The case $n = 2$ . For $n = 2$ the sum-zero lattice is $Z (1, - 1)$ , on which the transposition $(1 2)$ acts by $x \mapsto - x$ , the sign representation; this is the reduced summand of step 4.1. No choice principle is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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), and section 4 (Theorem 4.1) (standard reference, not scraped)