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

Free products and suitable amalgamated free products have solvable word problem

Statement

Let G and H be finitely generated groups with solvable word problem.

  1. The free product G∗H has solvable word problem.
  2. More generally, let a finitely generated group K embed in G and H. Assume membership in the two embedded copies of K is decidable, and that from a word in the generators of either factor representing an element of that copy one can compute a word in a fixed generating set of K representing the same element. Then the amalgamated free product G∗KH has solvable word problem.

Facts & Assumptions

Given: Finitely generated groups G,H, and in the second clause a finitely generated amalgamating group K with decidable membership in both images and effective translation of a discovered factor word in K back to a word in fixed generators of K.

[L1]

Every element of an amalgamated free product has a unique normal form relative to chosen transversals, and a normal word of positive length is nonidentity. (Normal form theorem for free products with amalgamation)

[L2]

The canonical maps of the factors into an amalgamated free product are injective. (The factor maps into a free product with amalgamation are injective)

Proof

technique · direct
1.1

In each factor, solvability of the word problem lets us compare any two words. Enumerating the words in shortlex order therefore computes a canonical representative for every group element, and in the amalgam case it also computes the least representative of every left coset of K: two words represent the same left coset exactly when their quotient lies in the embedded copy of K, which is decidable by hypothesis. The extra hypothesis also makes every factor word that represents an element of K effectively translatable into a canonical word in the fixed generators of K.

givenL2
2.1

For an input alternating word in the generators of the factors, first replace each factor block by its canonical representative. Whenever two consecutive blocks lie in the same factor, multiply them there and recanonize. In the amalgam case, if a block lies in the amalgamating subgroup, step 1.1 translates it to the canonical K-word and then into the generators of the opposite factor, so the amalgam relation pushes it across the next syllable effectively. The computable coset representatives from step 1.1 ensure that each such rewrite strictly shortens the syllable length.

L1step 1.1
3.1

The reduction process of step 2.1 halts with the normal form from [L1]. By uniqueness in [L1], the input represents the identity exactly when the final normal form has length zero and terminal K-part equal to the identity. Hence the procedure decides the word problem in G∗KH.

L1step 2.1
4.1

Taking K={e} gives the free-product case, so both clauses follow.

step 3.1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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