TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Boone special word equivalence

Statement

Assume AC. For every special word $Σ = X^{#} q_{j} Y$ , with $X, Y$ positive tape words, possibly empty, $W (Σ) = 1 in B ⟺ Σ^{*} = X q_{j} Y = q in Γ .$

Facts & Assumptions

Given: A positive special word $Σ$ in the stated domain.

[F1]

A positive semigroup history $Σ^{*} = q$ gives $Σ = L q R$ and $W (Σ) = 1$ . (Boone positive history pushing)

[F2]

$W (Σ) = 1$ gives $L Σ R = q$ in the embedded $G_{2}$ for freely reduced auxiliary words. (Boone commutator extracts an auxiliary history)

[F3]

Such an auxiliary equation for a special word gives $Σ^{*} = q$ in $Γ$ . (Boone positive history reconstruction)

[A1]

Assume AC for the HNN arguments in these facts. (The Axiom of Choice)

Proof

1.1

Suppose $W (Σ) = 1$ . The given positive special spelling satisfies the domain of [F2], so it supplies auxiliary $L, R$ with equality in $G_{2}$ . This is exactly the group and equation required by [F3], and that fact yields $Σ^{*} = q$ in $Γ$ .

F2F3A1given

2.1

Conversely, suppose $Σ^{*} = q$ . Equality in the presented semigroup is a finite symmetric history, and the special spelling has positive contexts. Thus [F1] applies and gives $W (Σ) = 1$ . The two implications include $X = Y = ε$ ; for $q_{j} = q$ they reduce to the defining commutation of $k$ and $q^{- 1} t q$ . This proves the stated equivalence on precisely the positive special-word domain.

F1A1step 1.1given∎

Source locator

Rotman, printed p.431, Lemma 12.7; proofs on pp.432–433 and pp.438–447. No equivalence for arbitrary signed tape words is asserted here.

Depends on

Used by

Novikov boone undecidability of the word problem Theorem

Dependency tree · two levels

12 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

Joseph J. Rotman, An Introduction to the Theory of Groups, Chapter 12, p.431, Lemma 12.7; pp.432–447, both proof directions (standard reference, not scraped)