ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge 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.

Baumslag-Solitar groups as HNN extensions

Example

For nonzero integers $m, n$ , the Baumslag-Solitar group

$B S (m, n) = ⟨ a, t ∣ t a^{m} t^{- 1} = a^{n} ⟩$

is an HNN extension of $Z$ , and it is ascending exactly in the cases $∣ m ∣ = 1$ or $∣ n ∣ = 1$ .

Facts & Assumptions

Given: Nonzero integers $m, n$ .

[L1]

A general HNN extension adjoins a stable letter conjugating one embedded subgroup onto another. (An HNN extension with its stable letter)

[L2]

An ascending HNN extension is the case in which one associated subgroup is the whole base group. (Ascending HNN extensions of injective endomorphisms)

[L3]

Ascending HNN extensions admit one-sided normal forms. (Ascending HNN extensions admit the one-sided normal form)

Verification

technique · direct

1.1L1given

In the base group $A = ⟨ a ⟩ ≅ Z$ , the subgroups $⟨ a^{m} ⟩$ and $⟨ a^{n} ⟩$ are isomorphic and the displayed presentation is exactly of the HNN form from [L1].

2.1L2L3step 1.1algebra∎

If $∣ m ∣ = 1$ , then $⟨ a^{m} ⟩ = A$ and [L2] makes $B S (m, n)$ an ascending HNN extension; similarly if $∣ n ∣ = 1$ after reversing the stable letter. In those cases [L3] gives the one-sided normal form. When both $∣ m ∣$ and $∣ n ∣$ exceed $1$ , both associated subgroups are proper, so the extension is not ascending.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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)