Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Conjugacy between cyclically Britton-reduced HNN words reduces to base-group conjugacy after cyclic permutation

Statement

Let u and v be cyclically Britton-reduced HNN words of positive stable-letter length in the associated-subgroup notation. If u and v are conjugate in the HNN extension, then some cyclic permutation u of u is conjugate to v by an element of the base group A.

Facts & Assumptions

Given: The cyclically Britton-reduced words u and v of positive stable-letter length.

[L1]

A cyclically Britton-reduced word has no pin across its two ends. (Cyclically Britton-reduced HNN words)

[L2]

Cyclic permutations of a positive-length cyclically Britton-reduced word are conjugate to it and remain cyclically Britton-reduced. (Cyclic permutations of a cyclically Britton-reduced HNN word stay in the same conjugacy class)

[L3]

Every element has a unique transversal normal form relative to chosen transversals. (Normal forms in an HNN extension are unique relative to chosen transversals)

Proof

technique · direct
1.1

We first record the boundary calculation used below. Let p=a0tε1a1tεnan be cyclically Britton-reduced with n>0, and write a positive-length Britton-reduced conjugator as y=btδz, where zt=yt1. At the two interfaces with p in y1py, only tδ and tδ from this first syllable of y can participate. A pin at the y1,p interface has the literal form tδ(b1a0)tε1 with ε1=δ; a pin at the p,y interface has the literal form tεn(anb)tδ with εn=δ. In either case the relation tct1=ϕ(c) or its inverse removes the displayed pair. The untouched copy of tδ becomes the opposite end syllable, and a direct substitution of the same relation shows that the remaining central word is a base-group conjugate of the corresponding literal cyclic permutation p1 of p. Absorb that base conjugacy into z to obtain y1py=y11p1y1 with y1t=yt1. The two signs cover the two associated subgroups, and [L1] and [L2] show that p1 is again cyclically Britton-reduced. If neither interface is a pin, the displayed word is Britton-reduced, because its three factors already are, and it has stable-letter length pt+2yt.

L1L2algebra
2.1

Let n=ut and r=vt. Among all equations y1py=q, with p a cyclic permutation of u, q a cyclic permutation of v, and y Britton-reduced, choose one minimizing yt; the original conjugacy supplies such an equation. If yt>0 and a boundary pin occurs, step 1.1 shortens y while rotating p, contrary to the choice. If no pin occurs, step 1.1 gives a Britton-reduced representative of q of length n+2yt. Normalizing a Britton-reduced word by [L3] only transfers associated-subgroup coefficients and performs no stable-letter cancellation, so uniqueness in [L3] gives r=n+2yt. Apply the same alternatives to p=yqy1. A boundary pin now shortens the same chosen conjugator while rotating q, again contradicting minimality; no boundary pin gives n=r+2yt, incompatible with the preceding equality. Thus yt=0, and [L3] also gives n=r.

L1L2L3step 1.1givenchoosealgebra
2.2

Now keep v fixed. Among all equations x1ux=v, with u a cyclic permutation of u and x Britton-reduced, choose one minimizing xt. Such equations exist by the hypothesis. If xt>0 and a boundary pin occurs, step 1.1 produces x11ux1=v with u a cyclic permutation of u and x1t=xt1, contradicting the choice.

L1L2step 1.1givenchoose
3.1

If instead no boundary pin occurs, step 1.1 makes x1ux a Britton-reduced word of length n+2xt. It represents v, whose Britton-reduced length is n by step 2.1. As in step 2.1, [L3] makes these lengths equal, a contradiction. Hence xt=0, so xA, and the chosen cyclic permutation u is conjugate to v by a base-group element as required.

L3step 1.1step 2.1step 2.2contradiction

Depends on

Used by

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