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

The full twist acts by boundary conjugation

Example

Let $Δ^{2} : = (σ_{1} σ_{2} \dots σ_{n - 1})^{n} \in B_{n}$ and $δ : = x_{1} x_{2} \dots x_{n} \in F_{n}$ . Then $ρ (Δ^{2}) (x_{i}) = δ x_{i} δ^{- 1} (1 \leq i \leq n);$ in particular the full twist acts by conjugation by the boundary word, which by The oriented boundary loop represents the ordered product of the standard meridians is the element $δ$ represented by the positively oriented boundary loop $\partial$ .

Facts & Assumptions

Given: the free group $F_{n} = ⟨ x_{1}, \dots, x_{n} ⟩$ with its reduced words, the automorphisms $ρ (σ_{i})$ of Artin automorphisms of the free group, the homomorphism $ρ : B_{n} \to Aut (F_{n})$ of The Artin representation on a free group, the braid $Γ : = σ_{1} σ_{2} \dots σ_{n - 1} \in B_{n}$ , and $δ_{m} : = x_{1} x_{2} \dots x_{m}$ for $0 \leq m \leq n$ , with $δ_{0} : = 1$ and $δ_{n} = δ$ .

[F1]

The substitutions. $ρ (σ_{i}) (x_{i}) = x_{i} x_{i + 1} x_{i}^{- 1}, ρ (σ_{i}) (x_{i + 1}) = x_{i}, ρ (σ_{i}) (x_{j}) = x_{j} (j \notin {i, i + 1}) .$ (Artin automorphisms of the free group.)

[F2]

The composite $U$ . $ρ$ is a homomorphism, so $U : = ρ (Γ) = ρ (σ_{1}) ρ (σ_{2}) \dots ρ (σ_{n - 1}) = ρ (σ_{1}) \circ ρ (σ_{2}) \circ \dots \circ ρ (σ_{n - 1})$ as functions on $F_{n}$ , and $ρ (Δ^{2}) = ρ (Γ^{n}) = U^{n}$ ; two endomorphisms of $F_{n}$ agree if they agree on the free basis $x_{1}, \dots, x_{n}$ . (The Artin representation on a free group, Free group on a set of generators.)

[F3]

The boundary word. The class $[x_{1}] \dots [x_{n}]$ corresponds to the positively oriented boundary loop $\partial$ under the identification of $π_{1} (D^{2} ∖ Q_{n}, d)$ with $F_{n}$ by the standard meridians (The oriented boundary loop represents the ordered product of the standard meridians, Standard meridians of a punctured disk).

Proof

Proof technique: induction on $m$ for the formula $U^{m} (x_{k}) = δ_{m} x_{k \oplus m} δ_{m}^{- 1} (0 \leq m \leq n, 1 \leq k \leq n),$ where $k \oplus m$ denotes the index obtained by adding $m$ to $k$ modulo $n$ in ${1, \dots, n}$ .

1.1F2base

Base case $m = 0$ . For $m = 0$ the formula reads $x_{k} = δ_{0} x_{k \oplus 0} δ_{0}^{- 1} = x_{k}$ , which holds since $U^{0} = id$ and $δ_{0} = 1$ .

1.2ih

Induction hypothesis. Assume that for some $m$ with $0 \leq m < n$ the formula $U^{m} (x_{k}) = δ_{m} x_{k \oplus m} δ_{m}^{- 1}$ holds for every $k$ .

1.3F1F2algebra

The action of $U$ on the generators and on $δ_{m}$ . By [F1], applying the factors of $U$ from the right (that is, $ρ (σ_{n - 1})$ first) to a basis letter gives $U (x_{k}) = x_{1} x_{k \oplus 1} x_{1}^{- 1} (1 \leq k \leq n),$ with the wrap convention $x_{n \oplus 1} = x_{1}$ : for $k < n$ the factors $ρ (σ_{n - 1}), \dots, ρ (σ_{k + 1})$ fix $x_{k}$ , the factor $ρ (σ_{k})$ sends $x_{k} \mapsto x_{k} x_{k + 1} x_{k}^{- 1}$ , and the factors $ρ (σ_{k - 1}), \dots, ρ (σ_{1})$ successively replace the left and right occurrences of $x_{k}$ by $x_{k - 1}, \dots, x_{1}$ , leaving $x_{1} x_{k + 1} x_{1}^{- 1}$ ; for $k = n$ the factors send $x_{n} \mapsto x_{n - 1} \mapsto \dots \mapsto x_{1}$ . Hence, multiplying the $m$ images and telescoping the inner conjugations, $U (δ_{m}) = U (x_{1}) \dots U (x_{m}) = (x_{1} x_{2} x_{1}^{- 1}) (x_{1} x_{3} x_{1}^{- 1}) \dots (x_{1} x_{m + 1} x_{1}^{- 1}) = δ_{m + 1} x_{1}^{- 1} .$

2.1step 1.2step 1.3algebra

The induction step. By the induction hypothesis of step 1.2 and the fact that $U$ is an automorphism, $U^{m + 1} (x_{k}) = U (δ_{m} x_{k \oplus m} δ_{m}^{- 1}) = U (δ_{m}) U (x_{k \oplus m}) U (δ_{m})^{- 1} .$ Substituting step 1.3 and using $(k \oplus m) \oplus 1 = k \oplus (m + 1)$ gives $U^{m + 1} (x_{k}) = (δ_{m + 1} x_{1}^{- 1}) (x_{1} x_{k \oplus (m + 1)} x_{1}^{- 1}) (x_{1} δ_{m + 1}^{- 1}) = δ_{m + 1} x_{k \oplus (m + 1)} δ_{m + 1}^{- 1} .$

3.1F2F3step 1.1step 2.1discharge-induction∎

Discharge and conclusion. Steps 1.1 and 2.1 establish the displayed formula for every $0 \leq m \leq n$ by induction; at $m = n$ it reads $U^{n} (x_{k}) = δ x_{k \oplus n} δ^{- 1} = δ x_{k} δ^{- 1}$ . By [F2] $ρ (Δ^{2}) = U^{n}$ , so $ρ (Δ^{2}) (x_{k}) = δ x_{k} δ^{- 1}$ for every $k$ ; by [F3] the element $δ$ is the boundary word, so the full twist acts by conjugation by it. For $n = 1$ there is no generator, $Δ^{2}$ is the empty product, $U = id$ and $δ = x_{1}$ , and the identity $ρ (1) (x_{1}) = x_{1} = δ x_{1} δ^{- 1}$ holds; for $n = 0$ the assertion is vacuous. All computations are finite substitutions in the free basis, and no choice principle is used.

Remarks

The exponent convention is the frozen one of Artin automorphisms of the free group: the leftmost letter of a word is the outermost automorphism of the composite, so that $U$ applies $ρ (σ_{n - 1})$ first. With the opposite (Artin's original) convention the same computation gives conjugation by $δ^{- 1}$ , which is the displayed formula of the scaffold record.
For $n = 2$ the formula is $ρ (σ_{1}^{2}) (x_{1}) = x_{1} x_{2} x_{1} x_{2}^{- 1} x_{1}^{- 1} = δ x_{1} δ^{- 1}$ with $δ = x_{1} x_{2}$ , and $ρ (σ_{1}^{2}) (x_{2}) = x_{1} x_{2} x_{1}^{- 1} = δ x_{2} δ^{- 1}$ , which is the same statement at rank two.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Juan Gonzalez-Meneses, Basic results on braid groups, section 1.6, printed pp. 8-10 (x_1...x_n runs parallel to the boundary and is preserved; the full twist acts as conjugation) (standard reference, not scraped)
Emil Artin, Theory of Braids, Annals of Mathematics 48 (1947), pp. 101-126, equations (14)-(15) and Theorem 15, printed pp. 112-114 (standard reference, not scraped)