Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03
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.

Reduced words form the free group on an alphabet

Statement

Let XX be a set. The reduced words on XX1X\sqcup X^{-1} form a group when the product of reduced words is their concatenation followed by free reduction. The map sending xXx\in X to the one-letter word xx has the universal property of the free group on XX.

Facts & Assumptions

Given: A set XX, its formal inverse alphabet, and a group GG with a function u:XGu:X\to G.

[L1]

Words, elementary cancellations, reduced words, and free equivalence are as in the reduced-word definition (Words in an alphabet with formal inverses, elementary cancellation, and reduced words).

[L2]

Induction proves a property of every finite word once it is proved for the empty word and preserved when one letter is appended (The principle of mathematical induction).

[L3]

A group has an associative operation with an identity and two-sided inverses, and a homomorphism preserves products (Group and abelian group, Monoid homomorphism and group homomorphism).

[L4]

The free-group universal property is the extension-and-uniqueness condition in the definition of a free group (Free group on a set of generators).

Proof

technique · direct
1.1

For a word ww, read its letters from left to right while maintaining a reduced stack: append a new letter unless it is the formal inverse of the stack's last letter, in which case delete that last letter. Induction on the length of ww gives a reduced output red(w)\operatorname{red}(w), with red(r)=r\operatorname{red}(r)=r for every reduced word rr.

L1L2
2.1

The same induction shows that reading a neighbouring pair aa1aa^{-1} or a1aa^{-1}a has exactly the same net effect on every preceding stack as omitting that pair. Thus red\operatorname{red} is unchanged by an elementary cancellation or reverse insertion; hence ww is freely equivalent to red(w)\operatorname{red}(w), and two freely equivalent reduced words are equal.

step 1.1L1L2
3.1

Let F(X)F(X) be the set of reduced words. For reduced r,sr,s, define rs:=red(rs)r\cdot s:=\operatorname{red}(rs), let the empty word be ee, and let r1r^{-1} be the reversal of rr with each letter formally inverted. Step 2.1 gives red(red(rs)t)=red(rst)=red(rred(st))\operatorname{red}(\operatorname{red}(rs)t)=\operatorname{red}(rst)=\operatorname{red}(r\operatorname{red}(st)).

step 2.1L1
4.1

The equality in step 3.1 makes the product associative. The empty word is a two-sided identity, and rr1rr^{-1} and r1rr^{-1}r reduce by successive central cancellations to the empty word; therefore every reduced word has the stated two-sided inverse. Hence F(X)F(X) is a group.

step 3.1L1L3
4.2

Send xXx\in X to the one-letter word xx. For u:XGu:X\to G, evaluate a word by replacing xx with u(x)u(x) and x1x^{-1} with u(x)1u(x)^{-1} and multiplying in order. Each elementary cancellation evaluates to an adjacent inverse pair, so evaluation is unchanged by step 2.1 and defines u^:F(X)G\widehat u:F(X)\to G; it extends uu and preserves the product by the definition in step 3.1.

step 2.1step 3.1L1L3given
5.1

Any homomorphism h:F(X)Gh:F(X)\to G extending uu is forced, by writing each reduced word as its ordered product of one-letter words and their inverses, to agree with the evaluation map of step 4.2. Thus u^\widehat u is unique.

step 4.1step 4.2L3
6.1

Steps 4.1--5.1 establish the group and the extension-and-uniqueness property of [L4], so the reduced-word group is the free group on XX.

step 4.1step 4.2step 5.1L4

Depends on

Used by

Cited to discharge well-definedness by Free group on a set of generators and Words in an alphabet with formal inverses, elementary cancellation, and reduced words.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 23 results over 12 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