CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

The Artin action solves the braid word problem

Statement

Assume AC. Given two words in $σ_{1}^{\pm 1}, \dots, σ_{n - 1}^{\pm 1}$ , the braids they represent are equal if and only if the corresponding automorphisms of $F_{n}$ agree on the generators $x_{1}, \dots, x_{n}$ . Since reduced words in a free group are unique and effectively computable, the word problem in $B_{n}$ is solvable. No choice principle beyond AC is used.

Facts & Assumptions

Given: AC, the Artin braid group $B_{n}$ on $σ_{1}, \dots, σ_{n - 1}$ , the free group $F_{n} = ⟨ x_{1}, \dots, x_{n} ⟩$ with its reduced words, and two braid words $β_{1}, β_{2}$ in the generators and their inverses.

[F1]

The representation. $ρ : B_{n} \to Aut (F_{n})$ is a well-defined group homomorphism, computed on a braid word by composing the automorphisms $ρ (σ_{i})^{\pm 1}$ attached to its letters; $ρ$ of the empty word is the identity, and $ρ (σ_{i}) (x_{i}) = x_{i} x_{i + 1} x_{i}^{- 1}, ρ (σ_{i}) (x_{i + 1}) = x_{i}, ρ (σ_{i}) (x_{j}) = x_{j} (j \notin {i, i + 1}) .$ (The Artin representation on a free group, Artin automorphisms of the free group.)

[F2]

Faithfulness. Assume AC. $ρ$ is injective: a braid word acts trivially on $F_{n}$ only if it represents the trivial element of $B_{n}$ . (The Artin representation is faithful.)

[F3]

Free groups and their word problem. An endomorphism of $F_{n}$ is determined by its values on the basis $x_{1}, \dots, x_{n}$ ; reduced words are unique representatives of elements of $F_{n}$ , and free reduction decides whether a word represents the identity, effectively. (Free group on a set of generators, Reduced words form the free group on an alphabet, The word problem for a finitely generated free group is solvable by free reduction.)

Proof

technique · direct

1.1F1F2F3algebra

The comparison criterion. Let $β_{1}, β_{2}$ be braid words. If $β_{1} = β_{2}$ in $B_{n}$ , then $ρ (β_{1}) = ρ (β_{2})$ because $ρ$ is a well-defined function, so the two automorphisms agree on every element of $F_{n}$ , in particular on the generators. Conversely, if $ρ (β_{1})$ and $ρ (β_{2})$ agree on the generators, then by [F3] they agree as endomorphisms of $F_{n}$ ; hence $ρ (β_{1} β_{2}^{- 1}) = ρ (β_{1}) ρ (β_{2})^{- 1} = id$ by [F1], and by faithfulness [F2] the braid word $β_{1} β_{2}^{- 1}$ represents the trivial element, that is, $β_{1} = β_{2}$ in $B_{n}$ .

1.2F1F3construct

Effectivity of the comparison. The $n$ images $ρ (β) (x_{j})$ of a braid word $β$ are computed letter by letter, substituting the finitely many displayed formulas of [F1] for the at most finitely many letters of $β$ and freely reducing; by [F3] the result is a unique reduced word representing the image. Comparing two braid words therefore amounts to computing and comparing $2 n$ reduced words, a finite and effective procedure.

2.1F2step 1.1step 1.2∎

Decision procedure and conclusion. Steps 1.1 and 1.2 give: the braids represented by $β_{1}$ and $β_{2}$ are equal if and only if the two automorphisms agree on $x_{1}, \dots, x_{n}$ , and this comparison is decided by the halting free-reduction algorithm. Hence the word problem in $B_{n}$ is solvable. The only use of AC is through the faithfulness theorem [F2]; the computation of the images and the free reduction are choice-free, so no choice principle beyond AC is used.

Remarks

This is Artin's original solution of the word problem, historically the first known; it is by no means efficient, but it is effective.
For $n \leq 1$ the group $B_{n}$ is trivial and both sides are trivial, so the criterion is vacuous; the substantive statement is for $n \geq 2$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Juan Gonzalez-Meneses, Basic results on braid groups, section 1.6.1, printed p. 9 (the first solution to the word problem in B_n via the Artin representation) (standard reference, not scraped)
Emil Artin, Theory of Braids, Annals of Mathematics 48 (1947), pp. 101-126, printed pp. 113-115 (standard reference, not scraped)