TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Every peripheral-boundary-preserving automorphism is an Artin automorphism

Statement

Every peripheral-boundary-preserving automorphism $A \in Aut (F_{n})$ (Peripheral-boundary-preserving automorphisms of F_n) equals $ρ (β)$ for some braid word $β$ , and $β$ may be chosen as a product of the generators $σ_{1}^{\pm 1}, \dots, σ_{n - 1}^{\pm 1}$ . No choice principle is used.

Facts & Assumptions

Given: a peripheral-boundary-preserving automorphism $A$ of $F_{n} = ⟨ x_{1}, \dots, x_{n} ⟩$ , written in the normalised reduced form $A (x_{i}) = Q_{i}^{- 1} x_{π (i)} Q_{i} (1 \leq i \leq n)$ with reduced words $Q_{i}$ , and with $A (x_{1} \dots x_{n}) = x_{1} \dots x_{n}$ .

[F1]

The length of $A$ . By Peripheral-boundary-preserving automorphisms of F_n the conjugators $Q_{i}$ may be chosen shortest, and changing a conjugator by a power of its middle generator does not change the conjugacy class; hence the minimal total length $ℓ (A) : = \min \sum_{i} ∣ Q_{i} ∣$ over all such representations is a well-defined nonnegative integer. A representation of total length $ℓ (A)$ is called minimal. (Peripheral-boundary-preserving automorphisms of F_n, An extremal cancellation shortens an Artin substitution.)

[F2]

The dichotomy. In a reduced conjugator representation of $\prod_{i} Q_{i}^{- 1} x_{π (i)} Q_{i} = x_{1} \dots x_{n}$ , either no adjacent junction cancellation deletes a middle letter, in which case $A = id$ and every $Q_{i}$ is empty; or choose the least qualifying adjacent pair and its first cancelled middle letter (Artin's product-cancellation dichotomy).

[F3]

Shortening. In the second case of [F2], postcomposition by $ρ (σ_{i})$ or its inverse, according to which middle letter is cancelled first, gives a peripheral-boundary-preserving $A^{'}$ with total conjugator length at least one smaller. Thus $A = A^{'} \circ ρ (σ_{i})^{ϵ}$ for $ϵ = \pm 1$ (An extremal cancellation shortens an Artin substitution, Artin automorphisms of the free group).

[F4]

The representation. $ρ : B_{n} \to Aut (F_{n})$ is a group homomorphism with $ρ (σ_{i})$ the explicit substitution of Artin automorphisms of the free group, so $ρ (β^{'} σ_{i}^{ϵ}) = ρ (β^{'}) ρ (σ_{i})^{ϵ}$ and $ρ (σ_{i}^{ϵ} β^{'}) = ρ (σ_{i})^{ϵ} ρ (β^{'})$ for every braid word $β^{'}$ and $ϵ = \pm 1$ ; and $ρ$ of the empty word is $id$ . (The Artin representation on a free group, The braid group by Artin presentation.)

[F5]

Reduced words. The words $x_{π (1)} x_{π (2)} \dots x_{π (n)}$ and $x_{1} x_{2} \dots x_{n}$ are reduced, and reduced words represent the same element only if they are equal (Reduced words form the free group on an alphabet, Free group on a set of generators).

Proof

technique · strong induction on the minimal total length $\ell(A)$

1.1F1F4F5base

Base case: $ℓ (A) = 0$ . If $ℓ (A) = 0$ , some representation has all $Q_{i} = 1$ , so $A (x_{i}) = x_{π (i)}$ for every $i$ ; the boundary condition gives $x_{π (1)} \dots x_{π (n)} = x_{1} \dots x_{n}$ , and by [F5] the two reduced words are equal, so $π = id$ and $A = id = ρ (empty word)$ . This covers $n = 0$ , where $F_{0}$ is trivial, and $n = 1$ , where every peripheral-boundary-preserving automorphism is the identity.

1.2ih

Induction hypothesis. Fix $m \geq 1$ and assume that every peripheral-boundary-preserving automorphism $A^{'}$ with $ℓ (A^{'}) < m$ equals $ρ (β^{'})$ for some braid word $β^{'}$ .

1.3F1F2

A minimal representation has a qualifying junction. Let $A$ have $ℓ (A) = m > 0$ and choose a representation of total length $m$ . The first case of [F2] would give all $Q_{i}$ empty, contrary to $m > 0$ . Thus its second case selects an adjacent pair whose junction cancellation deletes a middle letter.

2.1F3step 1.2step 1.3

Shortening. By [F3] there is a peripheral-boundary-preserving $A^{'}$ with $ℓ (A^{'}) \leq m - 1$ , and $A = A^{'} \circ ρ (σ_{i})^{ϵ}$ for $ϵ = \pm 1$ . The induction hypothesis gives $A^{'} = ρ (β^{'})$ .

3.1F4step 2.1

Recovering a braid word. By [F4], $A = ρ (β^{'}) \circ ρ (σ_{i})^{ϵ} = ρ (β^{'} σ_{i}^{ϵ})$ . This is a word in the required generators and their inverses.

4.1step 1.1step 1.2step 3.1discharge-induction∎

Discharge. The base case 1.1 settles $ℓ (A) = 0$ , and steps 1.3, 2.1 and 3.1 deduce the case $ℓ (A) = m$ from the induction hypothesis of step 1.2 for all smaller lengths; by induction on the nonnegative integer $ℓ (A)$ every peripheral-boundary-preserving automorphism is $ρ (β)$ for a braid word $β$ of the displayed form. Every argument used the explicit normal form, the finite cancellation analysis and the displayed substitutions, so no choice principle is used.

Remarks

This is the sufficiency half of Artin's characterization Artin's characterization of the braid subgroup of Aut(F_n); the necessity half is the choice-free lemma Artin automorphisms permute meridian conjugacy classes and fix the boundary word.
The proof uses neither completeness nor faithfulness of $ρ$ : the braid word is produced by the induction, not recognised by an injectivity statement. This is why the theorem is choice-free while the full characterization consumes AC through faithfulness.
Artin's subset variant uses the ordered sub-product and the corresponding braid generators for that subset of ends. It is not an assertion that the original adjacent generators suffice when nonconsecutive indices are retained.

Depends on

Used by

Artin's characterization of the braid subgroup of Aut(Fₙ) Theorem

Dependency tree · two levels

19 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

Emil Artin, Theory of Braids, Annals of Mathematics 48 (1947), pp. 101-126, Theorem 16 and its proof, printed pp. 113-115 (standard reference, not scraped)
Juan Gonzalez-Meneses, Basic results on braid groups, section 1.6, Theorem 1.3, printed p. 9 (standard reference, not scraped)