TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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.

$F_{w o r d} (X)$ is a group under $[w] [v] = [w v]$

Statement

For every set $X$ , $F_{w o r d} (X)$ is a group under $[w] [v] = [w v]$ . Its identity is the empty-word class $[ε]$ , and if $w = a_{1} \dots a_{n}$ , then

$[w]^{- 1} = [a_{n}^{- 1} \dots a_{1}^{- 1}] .$

Facts & Assumptions

Given: A set $X$ , the quotient $F_{w o r d} (X) = W (X) / \sim$ , and the class product of The word-quotient model $F_{w o r d} (X) : = W (X) / \sim$ with multiplication induced by concatenation.

[L1]

If $w \sim w^{'}$ and $v \sim v^{'}$ , then $w v \sim w^{'} v^{'}$ (Free equivalence is an equivalence relation and concatenation respects it).

[F1]

A group is a monoid $(G, *, e)$ in which every element is invertible (Group and abelian group).

Proof

technique · direct

1.1

If $[w] = [w^{'}]$ and $[v] = [v^{'}]$ , then $w \sim w^{'}$ and $v \sim v^{'}$ , so [L1] gives $w v \sim w^{'} v^{'}$ and therefore $[w v] = [w^{'} v^{'}]$ ; the class product is well-defined.

L1given

2.1

Literal string concatenation is associative, so for all word classes $([u] [v]) [w] = [(u v) w] = [u (v w)] = [u] ([v] [w])$ .

step 1.1algebra

2.2

The empty word satisfies $ε w = w = w ε$ , so $[ε] [w] = [w] = [w] [ε]$ .

step 1.1algebra

3.1

For $w = a_{1} \dots a_{n}$ , put $w^{*} = a_{n}^{- 1} \dots a_{1}^{- 1}$ ; successive cancellations from the central seam carry both $w w^{*}$ and $w^{*} w$ to $ε$ , including when $n = 0$ , so $[w] [w^{*}] = [ε] = [w^{*}] [w]$ .

givenstep 2.2

4.1

The product is well-defined and associative, $[ε]$ is a two-sided identity, and every $[w]$ has the two-sided inverse $[w^{*}]$ ; these are the group requirements in [F1].

F1step 1.1step 2.1step 2.2step 3.1∎

Depends on

Used by

The word-quotient group W(X)/∼ satisfies the universal property of the free group on X Theorem

Dependency tree · two levels

10 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

Nicholas Touikan, An Introduction to Combinatorial and Geometric Group Theory, §1.2 (standard reference, not scraped)

Fword(X)Fword​(X) is a group under [w][v]=[wv][w][v]=[wv]