ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Combing a four-strand braid word

Example

In $B_{4}$ consider the word $W = σ_{3} σ_{2} σ_{3} σ_{2}^{- 1} σ_{3}^{- 1} σ_{2}^{- 1} σ_{1} σ_{2} σ_{1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1} .$ Its first six letters cancel by one three-strand relation and the last six letters are $σ_{1} σ_{2} σ_{1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1}$ , itself trivial in $B_{3}$ by one three-strand relation, so $W$ traces the trivial geometric braid. Tracking the last point gives the position sequence $4, 3, 2, 2, 3, 4, 4, 4, 4, 4, 4, 4, 4;$ prefix insertion writes $W$ as a product of twelve combing factors, and the six-case reduction reduces them, in order, to $x_{3}, x_{2}, σ_{2}, x_{2}^{- 1}, x_{3}^{- 1}, σ_{2}^{- 1}, σ_{1}, σ_{2}, σ_{1}, σ_{2}^{- 1}, σ_{1}^{- 1}, σ_{2}^{- 1} .$ Collecting the $x$ -letters to the left gives $W \equiv W_{1} W_{2}$ with $W_{1} = x_{3} x_{2} x_{2}^{- 1} x_{3}^{- 1} x_{2} x_{2}^{- 1},$ which freely reduces to the empty word, and $W_{2} = σ_{1} σ_{2} σ_{1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1},$ which is trivial in $B_{3}$ by one three-strand relation. This is the first nontrivial instance of the combing algorithm: the word $W$ is not itself freely trivial, and after combing its two factors become trivial for two different reasons -- free cancellation for $W_{1}$ , the three-strand relation for $W_{2}$ -- which are exactly the two mechanisms the completeness proof uses.

Facts & Assumptions

Given: The group $B_{4} = ⟨ σ_{1}, σ_{2}, σ_{3} ⟩$ of The braid group by Artin presentation with its two Artin relations, the words $α_{j}, x_{j}$ of The Zariski combing words alpha_i and x_i in the Artin presentation for $n = 4$ , and the word $W$ displayed above.

[F1]

In $B_{4}$ the relations $σ_{i} σ_{i + 1} σ_{i} = σ_{i + 1} σ_{i} σ_{i + 1}$ and $σ_{i} σ_{j} = σ_{j} σ_{i}$ for $∣ i - j ∣ > 1$ hold, adjacent inverse $σ$ -pairs may be freely inserted and deleted, and the geometric assignment $φ_{4}$ sending $σ_{i}$ to the class of the elementary half twist is a homomorphism (The braid group by Artin presentation, The Artin presentation surjects onto the geometric braid group); in particular a word equivalent to the empty word by these moves represents the trivial geometric braid, and the geometric three-strand relation $σ_{i} σ_{i + 1} σ_{i} = σ_{i + 1} σ_{i} σ_{i + 1}$ holds among the half twists (The geometric three strand braid relation).

[F2]

The combing words satisfy $α_{j} = σ_{j} σ_{j + 1} \dots σ_{3}$ for $1 \leq j \leq 3$ , $α_{4} = 1$ , and $x_{j} = α_{j + 1}^{- 1} σ_{j}^{2} α_{j + 1}$ ; explicitly $α_{3} = σ_{3}$ , $α_{2} = σ_{2} σ_{3}$ , $α_{1} = σ_{1} σ_{2} σ_{3}$ , $x_{3} = σ_{3}^{2}$ , $x_{2} = σ_{3}^{- 1} σ_{2}^{2} σ_{3}$ and $x_{1} = σ_{3}^{- 1} σ_{2}^{- 1} σ_{1}^{2} σ_{2} σ_{3}$ (The Zariski combing words alpha_i and x_i in the Artin presentation).

[F3]

Prefix insertion: if $W$ is a word in $σ_{1}^{\pm 1}, \dots, σ_{3}^{\pm 1}$ whose geometric image is trivial, $j_{k}$ is the position of the tracked point after the first $k$ letters with $j_{0} = j_{12} = 4$ , and $F_{k} : = α_{j_{k - 1}}^{- 1} σ_{i_{k}}^{ε_{k}} α_{j_{k}}$ for the $k$ -th letter $σ_{i_{k}}^{ε_{k}}$ of $W$ , then $W$ is equivalent to $\prod_{k = 1}^{12} F_{k} = F_{1} F_{2} \dots F_{12}$ by insertions of pairs $α_{j} α_{j}^{- 1}$ (Prefix insertion rewrites a trivial braid word into combing factors).

[F4]

Six-case reduction: a combing factor $F = α_{j}^{- 1} σ_{k}^{ε} α_{j^{'}}$ , where $j^{'} = k + 1$ if $j = k$ , $j^{'} = k$ if $j = k + 1$ and $j^{'} = j$ otherwise, reduces using only the Artin relations and free cancellations to the empty word ( $j = k$ , $ε = 1$ ), to $x_{k}^{- 1}$ ( $j = k$ , $ε = - 1$ ), to $x_{k}$ ( $j = k + 1$ , $ε = 1$ ), to the empty word ( $j = k + 1$ , $ε = - 1$ ), to $σ_{k}^{ε}$ ( $k < j - 1$ ), and to $σ_{k - 1}^{ε}$ ( $k > j$ ) (Each combing factor reduces to a lower-rank letter or an x-letter).

[F5]

Conjugation table: for $1 \leq i \leq 2$ and $1 \leq j \leq 3$ , $σ_{i} x_{j} σ_{i}^{- 1}$ equals $x_{j}$ for $j < i$ or $j > i + 1$ , equals $x_{i}$ for $j = i + 1$ , and equals $x_{i}^{- 1} x_{i + 1} x_{i}$ for $j = i$ , using only the two Artin relations and free cancellations (Lower-rank Artin letters conjugate x-letters).

Verification

technique · direct

1.1F1

The two halves of $W$ are trivial. In $B_{4}$ the relation $σ_{3} σ_{2} σ_{3} = σ_{2} σ_{3} σ_{2}$ replaces the first three letters of $W$ , and then two free deletions give $σ_{2} σ_{3} σ_{2} σ_{2}^{- 1} σ_{3}^{- 1} σ_{2}^{- 1} \equiv σ_{2} σ_{3} σ_{3}^{- 1} σ_{2}^{- 1} \equiv σ_{2} σ_{2}^{- 1} \equiv 1$ ; the same relation with index $1$ gives $σ_{1} σ_{2} σ_{1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1} \equiv σ_{2} σ_{1} σ_{2} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1} \equiv σ_{2} σ_{1} σ_{1}^{- 1} σ_{2}^{- 1} \equiv 1$ for the last six letters. Hence $W$ is equivalent to the empty word, and $φ_{4} (W) = 1$ because $φ_{4}$ is a homomorphism: $W$ traces the trivial geometric braid.

2.1F3step 1.1

The position sequence. Since the geometric image of $W$ is trivial, the tracked point returns to its initial position, $j_{12} = j_{0} = 4$ . The letter $σ_{k}^{\pm 1}$ interchanges positions $k$ and $k + 1$ and fixes the others, so the tracked point passes from position $4$ to $3$ at the first letter $σ_{3}$ , from $3$ to $2$ at $σ_{2}$ , stays at $2$ under the next $σ_{3}$ , passes to $3$ at $σ_{2}^{- 1}$ and back to $4$ at $σ_{3}^{- 1}$ ; the remaining letters $σ_{2}^{- 1}$ and the six letters with index at most $2$ act only on the first three positions, so the tracked point stays at $4$ . The sequence is therefore $4, 3, 2, 2, 3, 4, 4, 4, 4, 4, 4, 4, 4$ .

3.1F2F3step 2.1

The twelve combing factors. With the positions of step 2.1 and $α_{4} = 1$ , $α_{3} = σ_{3}$ , $α_{2} = σ_{2} σ_{3}$ from [F2], [F3] writes $W$ as the product of the twelve factors $F_{k} = α_{j_{k - 1}}^{- 1} σ_{i_{k}}^{ε_{k}} α_{j_{k}}$ : $F_{1} = σ_{3}^{2}, F_{2} = σ_{3}^{- 1} σ_{2}^{2} σ_{3}, F_{3} = α_{2}^{- 1} σ_{3} α_{2}, F_{4} = σ_{3}^{- 1} σ_{2}^{- 2} σ_{3}, F_{5} = σ_{3}^{- 1} σ_{3}^{- 1},$ and $F_{6} = σ_{2}^{- 1}$ , $F_{7} = σ_{1}$ , $F_{8} = σ_{2}$ , $F_{9} = σ_{1}$ , $F_{10} = σ_{2}^{- 1}$ , $F_{11} = σ_{1}^{- 1}$ , $F_{12} = σ_{2}^{- 1}$ .

4.1F4step 3.1

Six-case reduction. By [F4], applied with the pair $(j, k, ε)$ of each factor: $F_{1} = α_{4}^{- 1} σ_{3} α_{3} = x_{3}$ and $F_{2} = α_{3}^{- 1} σ_{2} α_{2} = x_{2}$ (case $j = k + 1$ , $ε = 1$ ); $F_{3} = α_{2}^{- 1} σ_{3} α_{2}$ has $k = 3 > j = 2$ and reduces to $σ_{k - 1} = σ_{2}$ ; $F_{4} = α_{2}^{- 1} σ_{2}^{- 1} α_{3} = x_{2}^{- 1}$ and $F_{5} = α_{3}^{- 1} σ_{3}^{- 1} α_{4} = x_{3}^{- 1}$ (case $j = k$ , $ε = - 1$ ); and $F_{6}, \dots, F_{12}$ all have $k \leq 2 < j - 1 = 3$ (with $j = 4$ , so that $α_{j} = 1$ on both sides of the letter) and reduce to the letters $σ_{2}^{- 1}, σ_{1}, σ_{2}, σ_{1}, σ_{2}^{- 1}, σ_{1}^{- 1}, σ_{2}^{- 1}$ themselves. Hence $W \equiv x_{3} x_{2} σ_{2} x_{2}^{- 1} x_{3}^{- 1} σ_{2}^{- 1} σ_{1} σ_{2} σ_{1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1} .$

5.1F5step 4.1

Collecting the $x$ -letters. By [F5] with $i = 2$ : $σ_{2} x_{2} σ_{2}^{- 1} = x_{2}^{- 1} x_{3} x_{2}$ , hence $σ_{2} x_{2}^{- 1} = (x_{2}^{- 1} x_{3} x_{2})^{- 1} σ_{2} = x_{2}^{- 1} x_{3}^{- 1} x_{2} σ_{2}$ ; and $σ_{2} x_{3} σ_{2}^{- 1} = x_{2}$ , hence $σ_{2} x_{3}^{- 1} = x_{2}^{- 1} σ_{2}$ . Substituting these two identities into the word of step 4.1, $x_{3} x_{2} (σ_{2} x_{2}^{- 1}) x_{3}^{- 1} σ_{2}^{- 1} (rest) \equiv x_{3} x_{2} x_{2}^{- 1} x_{3}^{- 1} x_{2} (σ_{2} x_{3}^{- 1}) σ_{2}^{- 1} (rest) \equiv x_{3} x_{2} x_{2}^{- 1} x_{3}^{- 1} x_{2} x_{2}^{- 1} σ_{2} σ_{2}^{- 1} (rest),$ where $(rest) = σ_{1} σ_{2} σ_{1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1}$ ; deleting the adjacent pair $σ_{2} σ_{2}^{- 1}$ gives $W \equiv W_{1} W_{2}$ with $W_{1} = x_{3} x_{2} x_{2}^{- 1} x_{3}^{- 1} x_{2} x_{2}^{- 1}$ and $W_{2} = σ_{1} σ_{2} σ_{1} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1}$ .

6.1F4F5step 5.1

Both factors are trivial. The word $W_{1}$ reduces to the empty word by the free cancellations $x_{2} x_{2}^{- 1}$ and $x_{3} x_{3}^{- 1}$ : $x_{3} x_{2} x_{2}^{- 1} x_{3}^{- 1} x_{2} x_{2}^{- 1} \equiv x_{3} x_{3}^{- 1} x_{2} x_{2}^{- 1} \equiv 1$ . The word $W_{2}$ is trivial in the rank-3 subgroup: the braid relation $σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2}$ gives $W_{2} \equiv σ_{2} σ_{1} σ_{2} σ_{2}^{- 1} σ_{1}^{- 1} σ_{2}^{- 1} \equiv σ_{2} σ_{1} σ_{1}^{- 1} σ_{2}^{- 1} \equiv 1$ . Thus the combing algorithm decomposes $W$ into a factor that is freely trivial in the $x$ -letters and a factor that is trivial on the lower rank, which is exactly the mechanism of Every trivial braid word combs as W_1W_2 and of the completeness theorem; the example illustrates that a word can fail to be freely trivial after combing while both of its combed factors are accounted for. ∎

Remarks

The example is choice-free: every move is an explicit word computation in $B_{4}$ , and the only geometric input is the published validity of the three-strand relation and of the surjection $φ_{4}$ , which are used to record that the triviality of $W$ in $B_{4}$ matches the triviality of the geometric braid.
The three-strand relation appears twice for different purposes: inside step 1.1 it shows that $W$ itself is already trivial, while inside step 6.1 it shows that the lower-rank factor $W_{2}$ is trivial, which is the input the induction of the completeness theorem consumes.

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 3.1, printed pp. 19-22 (standard reference, not scraped)