Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-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.

Fword(X)F_{\mathrm{word}}(X) is a group under [w][v]=[wv][w][v]=[wv]

Statement

For every set XX, Fword(X)F_{\mathrm{word}}(X) is a group under [w][v]=[wv][w][v]=[wv]. Its identity is the empty-word class [ε][\varepsilon], and if w=a1⋯anw=a_1\cdots a_n, then

[w]−1=[an−1⋯a1−1].[w]^{-1}=[a_n^{-1}\cdots a_1^{-1}].

Facts & Assumptions

Given: A set XX, the quotient Fword(X)=W(X)/∼F_{\mathrm{word}}(X)=W(X)/{\sim}, and the class product of The word-quotient model Fword(X):=W(X)/∼F_{\mathrm{word}}(X):=W(X)/{\sim} with multiplication induced by concatenation.

[L1]

If w∼w′w\sim w' and v∼v′v\sim v', then wv∼w′v′wv\sim w'v' (Free equivalence is an equivalence relation and concatenation respects it).

[F1]

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

Proof

technique · direct
1.1

If [w]=[w′][w]=[w'] and [v]=[v′][v]=[v'], then w∼w′w\sim w' and v∼v′v\sim v', so [L1] gives wv∼w′v′wv\sim w'v' and therefore [wv]=[w′v′][wv]=[w'v']; the class product is well-defined.

L1given
2.1

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

step 1.1algebra
2.2

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

step 1.1algebra
3.1

For w=a1⋯anw=a_1\cdots a_n, put w∗=an−1⋯a1−1w^*=a_n^{-1}\cdots a_1^{-1}; successive cancellations from the central seam carry both ww∗ww^* and w∗ww^*w to ε\varepsilon, including when n=0n=0, so [w][w∗]=[ε]=[w∗][w][w][w^*]=[\varepsilon]=[w^*][w].

givenstep 2.2
4.1

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

F1step 1.1step 2.1step 2.2step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

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