DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28

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.

HNN words, pins, and Britton-reduced words

Definition

Work in the associated-subgroup notation of The edge-group presentation is equivalent to the associated-subgroup presentation:

$G = ⟨ A, t ∣ t c t^{- 1} = ϕ (c) for c \in C_{-} ⟩,$

where $ϕ : C_{-} \to C_{+}$ is an isomorphism.

An HNN word is an expression

$a_{0} t^{ε_{1}} a_{1} \dots t^{ε_{n}} a_{n},$

with $n \geq 0$ , $a_{i} \in A$ , and $ε_{i} \in {1, - 1}$ . Its stable-letter length is $n$ .

A pin is a subword of one of the two forms

$t c t^{- 1} (c \in C_{-}),$

$t^{- 1} d t (d \in C_{+}) .$

An HNN word is Britton-reduced when no pin occurs and every interior base coefficient $a_{i}$ with $1 \leq i < n$ is nonidentity whenever $ε_{i} = - ε_{i + 1}$ . Equivalently, a sign change is allowed only across a coefficient that does not lie in the subgroup that would create a pin.

Depends on

The edge-group presentation is equivalent to the associated-subgroup presentation

Used by

A stable-letter word need not be Britton-reduced Counterexample
Cyclically Britton-reduced HNN words Definition
Britton reduction of a word with two pins Example
FALSE: every word containing a stable letter is nontrivial False statement
Elementary HNN reductions preserve the represented element Lemma
Britton's lemma Theorem

Dependency tree · two levels

5 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

Roger C. Lyndon and Paul E. Schupp, Combinatorial Group Theory (standard reference, not scraped)