LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

Every nonempty reduced word has the form $tct^{-1}$ with $c$ nonempty and cyclically reduced

Statement

Every nonempty reduced word $w$ has a literal factorisation

$w=tct^{-1}$

in which $c$ is nonempty and cyclically reduced. The displayed concatenation is the original reduced word, with no hidden cancellation. In particular, $w$ is conjugate to $c$ in the reduced-word free group.

Facts & Assumptions

Given: A nonempty reduced word $w$ on $X\sqcup X^{-1}$ .

[F1]

A reduced word is cyclically reduced when it is empty or its first letter is not the formal inverse of its last letter (Cyclically reduced words).

[L1]

If a property $P$ satisfies $P(0)$ and $P(n)\Rightarrow P(n+1)$ for every natural number $n$ , then $P(n)$ holds for every $n\in\mathbb N$ (The principle of mathematical induction).

[L2]

The reduced words on $X\sqcup X^{-1}$ form a group when the product of reduced words is their concatenation followed by free reduction, and the map sending $x\in X$ to the one-letter word $x$ has the universal property of the free group on $X$ (Reduced words form the free group on an alphabet).

Proof

technique · induction

1.1

A reduced word of length one is nonempty and cyclically reduced, so the assertion holds with $t=\varepsilon$ and $c=w$ .

baseF1

1.2

Assume the assertion for all nonempty reduced words shorter than $w$ . If $w$ is cyclically reduced, take $t=\varepsilon$ and $c=w$ .

ihF1

1.3

If $w$ is not cyclically reduced, [F1] says that its first and last letters are inverse, so $w=aua^{-1}$ literally; reducedness of $w$ makes $u$ nonempty and reduced, and $|u|=|w|-2$ .

F1given

2.1

Apply [L1] to the property that the assertion holds at every length at most $n$ . The induction hypothesis then applies to the shorter word $u$ , so write $u=t'c(t')^{-1}$ with $c$ nonempty and cyclically reduced; then $w=(at')c(at')^{-1}$ literally.

step 1.2step 1.3L1

3.1

The alternatives in steps 1.2 and 2.1 cover every nonempty reduced word and give the required factorisation, including the one-letter boundary.

step 1.1step 1.2step 2.1

4.1

In the group of [L2] the product of reduced words is their concatenation followed by free reduction. The concatenation $t\,c\,t^{-1}$ is the reduced word $w$ of step 3.1, so no reduction occurs there and that product is $w$ ; the concatenation $t\,t^{-1}$ reduces to the empty word, which is the identity because concatenating it with any reduced word changes nothing, so $t^{-1}$ is the inverse of $t$ . Hence $w=tct^{-1}$ exhibits $w$ as a conjugate of $c$ in that group.

L2step 3.1algebradischarge-induction∎

Depends on

Used by

Free groups are torsion-free Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 22 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Wilhelm Magnus, Abraham Karrass, and Donald Solitar, Combinatorial Group Theory (standard reference, not scraped)
Alexei Myasnikov and Vladimir Shpilrain, Combinatorics over Free Groups, §2.2.1 (standard reference, not scraped)

Every nonempty reduced word has the form tct−1tct^{-1}tct−1 with ccc nonempty and cyclically reduced