TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Braid groups are torsion free by the garside lattice

Statement

Let $n \geq 0$ and let $B_{n}$ be the braid group of The braid group by Artin presentation. If $x \in B_{n}$ and $x^{r} = 1$ for some integer $r \geq 1$ , then $x = 1$ . Equivalently, $B_{n}$ is torsion free: its only element of finite order is the identity.

The proof uses the fact that the left divisibility order of Left and right divisibility extend to lattice orders on the braid group makes $B_{n}$ a lattice in which left translations are lattice automorphisms, and it does not use the normal form of Left garside normal form is unique. For $n = 0, 1$ the group $B_{n}$ is trivial, since its presentation has no generator, and the assertion holds vacuously. No choice principle is used.

Facts & Assumptions

Given: A natural number $n \geq 0$ , the braid group $B_{n}$ , an element $x \in B_{n}$ and an integer $r \geq 1$ with $x^{r} = 1$ .

[F1]

$B_{n}$ is a group, with $x^{0} = 1$ and $x^{r} = x x^{r - 1}$ for $r \geq 1$ ; elements can be cancelled in a group ( $y d = z d$ implies $y = z$ ).

[F2]

The left divisibility order $≼_{L}$ on $B_{n}$ of Left and right divisibility extend to lattice orders on the braid group is a partial order under which every pair of elements has a greatest lower bound $u \land_{L} v$ and a least upper bound, and every left translation is a lattice automorphism: $z (u \land_{L} v) = z u \land_{L} z v$ for all $u, v, z \in B_{n}$ . Consequently every nonempty finite family has a greatest lower bound, obtained by iterating the binary meet.

[F3]

For $n = 0$ and $n = 1$ the presentation of The braid group by Artin presentation has no generator and no relation, so $B_{n}$ is the trivial group.

Proof

technique · direct

1.1

The case $n \leq 1$ . If $n = 0$ or $n = 1$ , then $B_{n}$ is trivial by [F3], so its only element is $1$ and the statement is vacuous.

1.2

The meet of the orbit. Let $n \geq 2$ and $x^{r} = 1$ with $r \geq 1$ . The family ${1, x, x^{2}, \dots, x^{r - 1}}$ is finite and nonempty, so its greatest lower bound $d : = 1 \land_{L} x \land_{L} x^{2} \land_{L} \dots \land_{L} x^{r - 1}$ exists and is unique by [F2] (for $r = 1$ the family is ${x^{0}} = {1}$ and $d = 1$ ; for $r \geq 2$ iterate the binary meet).

F1F2

2.1

Left multiplication permutes the family. By [F2], left multiplication by $x$ distributes over finite meets, so $x d = x \land_{L} x^{2} \land_{L} \dots \land_{L} x^{r - 1} \land_{L} x^{r} = x \land_{L} x^{2} \land_{L} \dots \land_{L} x^{r - 1} \land_{L} 1$ , where the last step uses $x^{r} = 1$ [F1]. The family ${x, x^{2}, \dots, x^{r - 1}, 1}$ is the same set as ${1, x, \dots, x^{r - 1}}$ , and the meet does not depend on the order in which the binary meets are taken by [F2]; hence $x d = d$ .

F1F2step 1.2

3.1

Cancellation. Since $x d = d = 1 \cdot d$ , cancelling $d$ on the right in the group [F1] gives $x = 1$ . Hence a braid of finite order $r \geq 1$ is trivial; equivalently, no nonidentity element of $B_{n}$ has finite order.

F1step 2.1

4.1

Assembly. Step 1.1 disposes of $n \leq 1$ and step 3.1 of $n \geq 2$ , so every element of finite order in $B_{n}$ is the identity. The only structural input is the group lattice of [F2] and its compatibility with left multiplication; no positivity of $x$ , no normal form and no geometric model is used. In particular the argument also applies verbatim to every Garside group whose left order is a lattice with left translations acting by lattice automorphisms. No choice principle is used. ∎

step 1.1step 1.2step 2.1step 3.1

Remarks

Why the meet is stable. The identity $x (1 \land x \land \dots \land x^{r - 1}) = x \land x^{2} \land \dots \land x^{r}$ is the whole argument: the cyclic shift of the family ${1, x, \dots, x^{r - 1}}$ produces the same set, so $x d = d$ and cancellation finishes. This is Garside's fourth proof of torsion freeness, as reproduced in J. González-Meneses, Basic results on braid groups, Proposition 4.1, printed p. 30.
Consistency with the centre. Together with The center of b n is generated by the full twist for n greater than two this shows that $⟨ Δ^{2} ⟩$ is infinite cyclic, since $Δ^{2} \neq 1$ and no nonidentity braid has finite order; this is used in the companion example page.
Nothing here uses the Axiom of Choice or any weaker choice principle: the meet is taken over a finite family listed from the given element $x$ .

Depends on

Used by

The center of b n is generated by the full twist for n greater than two Theorem

Dependency tree · two levels

11 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

J. Gonzalez-Meneses, Basic results on braid groups, Proposition 4.1, printed p. 30 (standard reference, not scraped)