ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-10-02

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.

Standard $A_{i j}$ as point pushes after relabeling

Example

Assume the Axiom of Choice, let $n \geq 2$ and $1 \leq i < j \leq n$ , and use the base configuration $Q = (q_{1}, \dots, q_{n})$ and positive half twists of The elementary geometric half twist, its support disc, and its opposite. The standard pure braid $A_{i j} \in P B_{n}$ is the image of the geometric word $W_{i j}$ of Standard geometric pure braid generators A_ij. Put $Y^{(j)} : = int D^{2} ∖ {q_{k} : k \neq j} .$ For a based loop $γ$ of $Y^{(j)}$ at $q_{j}$ , let $M_{j} (γ) (t) : = (q_{1}, \dots, q_{j - 1}, γ (t), q_{j + 1}, \dots, q_{n}) \in F_{n} (int D^{2}) .$ This is the ordered motion in which only the $j$ -th point moves.

Choose the compatible family of local meridian circles and stems constructed by the puncture-avoiding fan argument in the proof of The $A_{i n}$ are meridian generators of the forgetful free kernel. Thus, for each $r < n$ , take $0 < ϵ_{r} \leq h_{n} / 10$ , let $C_{r} = {z : ∣ z - q_{r} ∣ = ϵ_{r}}$ and $c_{r} = q_{r} + (ϵ_{r}, 0)$ , and use the local stem $τ_{r}$ from $q_{r + 1}$ to $c_{r}$ selected in that compatible family, inside $U_{r} ∖ {q_{r}}$ . For $i < j$ , let $h_{i, j} : = H_{j - 1} \circ \dots \circ H_{i + 1},$ where $H_{s}$ represents the positive half twist $σ_{s}$ and the empty composition for $j = i + 1$ is the identity. The associated meridian stem from $q_{j}$ to $C_{i}$ is $h_{i, j} \circ τ_{i}$ ; let $γ_{i, j}^{c w}$ be the based loop that follows this stem, traverses $C_{i}$ clockwise once, and returns along the reverse stem. These are the compatible standard meridian stems obtained by transporting the adjacent local stem through the successive half twists. Then:

Point push. For every $1 \leq i < j \leq n$ , $A_{i j} = ι_{*}^{F} [M_{j} (γ_{i, j}^{c w})] \in P B_{n} .$ Thus the positive standard generator is the class of the motion that holds the other $n - 1$ labelled points fixed and moves the $j$ -th point clockwise once around $q_{i}$ along the stated stem.
Relabeled form. Let $ρ \in S_{n}$ satisfy $ρ (j) = n$ , $ρ (k) = k - 1$ for $j < k \leq n$ , and $ρ (k) = k$ for $k < j$ . The coordinate permutation $(R x)_{k} : = x_{ρ^{- 1} (k)}$ gives homeomorphisms $R^{\circ}$ and $R^{D}$ on the open and closed ordered configuration spaces, respectively. It takes $Q$ to $Q^{ρ} = (q_{1}, \dots, q_{j - 1}, q_{j + 1}, \dots, q_{n}, q_{j}) .$ Put $Y^{ρ} : = int D^{2} ∖ {q_{k} : k \neq j}$ , and define the open terminal-coordinate inclusion ${\tilde{κ}}^{ρ} : π_{1} (Y^{ρ}, q_{j}) ⟶ π_{1} (F_{n} (int D^{2}), Q^{ρ}), [γ] ⟼ [(q_{1}, \dots, q_{j - 1}, q_{j + 1}, \dots, q_{n}, γ)] .$ With $ι_{*}^{F, ρ}$ the open-to-closed map at basepoint $Q^{ρ}$ , set $κ^{ρ} : = ι_{*}^{F, ρ} \circ {\tilde{κ}}^{ρ}$ . Then $R_{*}^{D} (A_{i j}) = κ^{ρ} ([γ_{i, j}^{c w}]) \in π_{1} (F_{n} (D^{2}), Q^{ρ}),$ the loop class in which the last coordinate moves clockwise around $q_{i}$ and all other coordinates remain fixed.
Terminal mapping-class sign. For $i < n$ , $Θ_{n} (A_{i n}) = {Push}_{n} ([γ_{i, n}^{c w}]), Θ_{n} : = Ψ_{n}^{m c} \circ (Ψ_{n}^{c o n f})^{- 1},$ where $Θ_{n}$ is the isomorphism of Point pushing is the kernel of forgetting the last disk puncture. The inverse-endpoint convention in Point pushing the last puncture makes the clockwise fibre meridian correspond to the positive generator. The raw ordered slice of the positive standard word runs counterclockwise; the configuration identification inverts that slice.

Facts & Assumptions

Given: AC, $n \geq 2$ , $1 \leq i < j \leq n$ , the base configuration $Q$ , the half twists $σ_{1}, \dots, σ_{n - 1}$ and their supports $U_{1}, \dots, U_{n - 1}$ , the words $W_{i j}$ , and the maps in the statement.

[A1]

The Axiom of Choice holds (The Axiom of Choice).

[F1]

In ZF, AC implies DC and DC implies countable choice (AC implies DC implies countable choice).

[F2]

The Statement of The $A_{i n}$ are meridian generators of the forgetful free kernel says that, under AC, the last-coordinate fibre inclusion $κ$ identifies $F_{m - 1}$ with the kernel of forgetting $P B_{m} \to P B_{m - 1}$ , and the $m - 1$ configuration-group images $Ψ ([A_{1 m}]), \dots, Ψ ([A_{m - 1, m}])$ of the standard geometric classes form a free basis. For the compatible stem family constructed in its proof, if $[λ_{r}]$ is the counterclockwise meridian class in the fibre, then $Ψ ([A_{r m}]) = (κ_{*} [λ_{r}])^{- 1} .$ Here $[A_{r m}] = [W_{r m}]$ is the geometric braid class and, by [F3], its configuration-group image is the element denoted $A_{r m}$ in this example; $κ_{*} [λ]$ is the closed-disc image of the open fibre loop. The supplier Statement makes this last-column assertion; its proof also supplies the local winding and conjugation arguments used below for arbitrary $j$ . It does not assert that the whole word motion is braid-isotopic to a one-coordinate motion.

[F3]

The standard generators are $A_{r s} = Ψ_{n}^{c o n f} ([W_{r s}])$ , where $W_{r s} = σ_{s - 1} \dots σ_{r + 1} σ_{r}^{2} σ_{r + 1}^{- 1} \dots σ_{s - 1}^{- 1} .$ The rightmost factor is the bottom one, $[γ ⋆ β] = [γ] [β]$ , and $Ψ_{n}^{c o n f} ([β]) = (ι_{*}^{F} [z_{β}])^{- 1}$ for the ordered coordinate loop $z_{β}$ (Standard geometric pure braid generators A_ij, Pure geometric braids and ordered configuration loops).

[F4]

The positive half twist $σ_{r}$ exchanges $q_{r}, q_{r + 1}$ , is supported in $U_{r} = B (m_{r}, 3 h_{n} / 2)$ , and fixes every other base point; $U_{r} \cap U_{s} = \emptyset$ when $∣ r - s ∣ > 1$ . Here the base points are equally spaced by $2 h_{n}$ , so the center of $U_{r + 1}$ is distance $3 h_{n}$ from $q_{r}$ (The elementary geometric half twist, its support disc, and its opposite).

[F5]

Geometric braids form a group under stacking, with the right factor running first; coordinate paths of pure braids are loops in $F_{n} (int D^{2})$ , and reversed braid paths represent inverse classes (The isotopy classes of geometric braids based at $Q$ form a group, and the endpoint permutation is a homomorphism, Stacking of geometric braids is a well-defined associative operation on isotopy classes).

[F6]

Coordinate permutations act by homeomorphisms on both $F_{n} (int D^{2})$ and $F_{n} (D^{2})$ , and the open-to-closed inclusions commute with these permutations (The symmetric group acts continuously and freely on $F_{n} (X)$ by permuting labels, The interior-disc and closed-disc configuration spaces are homotopy equivalent).

[F7]

The maps $Ψ_{n}^{c o n f} : G_{n}^{p u r e} \to P B_{n}$ and $Ψ_{n}^{m c} : G_{n} \to Mod (D^{2}, Q; \partial D^{2})$ are group isomorphisms, with $Ψ_{n}^{c o n f} ([β]) = (ι_{*}^{F} [z_{β}])^{- 1}$ and, for the raw unordered slice $S (β)$ , $Ψ_{n}^{m c} ([β]) = δ ([S (β)]^{- 1})$ ; on a half twist, $Ψ_{n}^{m c} ([σ_{r}]) = [H_{r}]$ , where $H_{r}$ is orientation-preserving, supported in $U_{r}$ , and exchanges $q_{r}, q_{r + 1}$ (Pure geometric braids and ordered configuration loops, Braid group as boundary-fixed punctured-disk mapping classes).

[F8]

The point-pushing map for the last puncture is ${Push}_{n} ([γ]) = δ ([\overset{ˉ}{γ}])$ , where $\overset{ˉ}{γ}$ is the unordered loop of the ordered motion that moves only $q_{n}$ and $δ$ is the inverse-endpoint boundary map. The braid-to-mapping-class map sends that raw geometric motion to $δ ([\overset{ˉ}{γ}]^{- 1}) = {Push}_{n} ([γ])^{- 1}$ (Point pushing the last puncture, Boundary map from point motions).

[F9]

Under AC, $Θ_{n} = Ψ_{n}^{m c} ∣_{G_{n}^{p u r e}} \circ (Ψ_{n}^{c o n f})^{- 1}$ is an isomorphism and $Θ_{n} \circ κ = {Push}_{n}$ for the terminal-coordinate fibre inclusion (Point pushing is the kernel of forgetting the last disk puncture).

[F10]

$F_{n} (X)$ is the space of pairwise distinct tuples in $X^{n}$ , $P B_{n} = π_{1} (F_{n} (D^{2}), Q)$ , and $ι_{*}^{F} : π_{1} (F_{n} (int D^{2}), Q) \to P B_{n}$ is an isomorphism (Ordered configuration spaces $F_{n} (X)$ , The pure braid group $P B_{n}$ as the fundamental group of an ordered configuration space, The interior-disc and closed-disc configuration spaces are homotopy equivalent).

[F11]

The local two-point winding computation in the proof of The $A_{i n}$ are meridian generators of the forgetful free kernel identifies $F_{2} (U_{r}) ≅ S^{1} \times C$ with $C$ convex and shows that the raw coordinate loop of $σ_{r}^{2}$ has relative winding $+ 1$ , equal to a counterclockwise local meridian motion of $q_{r + 1}$ around $q_{r}$ . By the inverse-endpoint convention, $Ψ_{n}^{m c} ([σ_{r}^{2}]) = {Push}_{q_{r + 1}} ([λ_{r}^{c c w}])^{- 1} = {Push}_{q_{r + 1}} ([λ_{r}^{c w}]) .$ The proof's conjugation argument establishes, for any mapping class $h$ taking a marked point $p$ to $p^{'}$ , the typed naturality $h {Push}_{p} ([α]) h^{- 1} = {Push}_{p^{'}} ([h \circ α]),$ where $α$ is a loop in the complement of $Q ∖ {p}$ based at $p$ and $h \circ α$ is based at $p^{'}$ in the complement of $Q ∖ {p^{'}}$ . There ${Push}_{p}$ is the inverse endpoint of an ambient lift of this single-point motion; for $p = q_{n}$ it agrees with [F8].

Verification

technique · direct

Choice bookkeeping. AC supplies DC and countable choice, so the cited fibre exact sequence, braid identifications, and point-pushing identifications are available. [A1, F1, F2, F7, F9]

1.1A1F1F2F7F9

The choice hypothesis discharges the cited fibration and mapping-class identifications.

Terminal fibre case. Fix $i < n$ and let $[λ_{i}^{c c w}]$ be the counterclockwise based meridian class in the last-coordinate fibre at $q_{n}$ from [F2]. Write $[λ_{i}^{c w}] = [λ_{i}^{c c w}]^{- 1}$ . The standard generator in $P B_{n}$ is $A_{i n} = Ψ_{n}^{c o n f} ([W_{i n}])$ ; applying $Ψ_{n}^{c o n f}$ to $A_{i n}$ again would be ill-typed. The source formula and the fact that the fibre inclusion is a homomorphism give $A_{i n} = (κ_{*} [λ_{i}^{c c w}])^{- 1} = κ_{*} [λ_{i}^{c w}] = ι_{*}^{F} [M_{n} (λ_{i}^{c w})] .$ This proves the terminal instance of claim 1. [F2, F3, F10]

2.1step 1.1F2F3F10

Thus the terminal generator is the closed-disc image of the clockwise last-coordinate meridian.

A point-motion loop maps to its point push. Let $p = q_{j}$ and let $γ$ be any based loop in $Y^{(j)}$ at $q_{j}$ . By the geometric-braid/configuration identification [F3] and the open-to-closed map [F10], the ordered loop $M_{j} (γ)$ defines a pure geometric braid $β_{γ}$ whose unordered slice is $\overset{ˉ}{γ}$ . Its inverse braid $β_{γ}^{- 1}$ has coordinate loop class $[M_{j} (γ)]^{- 1}$ and unordered slice class $[\overset{ˉ}{γ}]^{- 1}$ . The braid/configuration and braid/mapping-class maps [F7] therefore give $Ψ_{n}^{c o n f} (β_{γ}^{- 1}) = (ι_{*}^{F} [M_{j} (γ)]^{- 1})^{- 1} = ι_{*}^{F} [M_{j} (γ)], Ψ_{n}^{m c} (β_{γ}^{- 1}) = δ (([\overset{ˉ}{γ}]^{- 1})^{- 1}) = δ ([\overset{ˉ}{γ}]) .$ For any marked point $q_{j}$ , the inverse-endpoint point-motion map constructed in the kernel lemma's proof is ${Push}_{q_{j}} ([γ]) = δ ([\overset{ˉ}{γ}])$ ; for $j = n$ this agrees with [F8]. Thus $Θ_{n} (ι_{*}^{F} [M_{j} (γ)]) = Ψ_{n}^{m c} (β_{γ}^{- 1}) = {Push}_{q_{j}} ([γ]) .$ This identity will compare classes by the isomorphism $Θ_{n}$ and uses no fibre-inclusion injectivity. [F3, F7, F8, F10, F11]

2.2step 1.1F3F7F8F10F11

For every marked point, the image under $Θ_{n}$ of its one-coordinate motion is the corresponding point push.

Transport the adjacent point push. Fix $i < j$ . Choose the local circle $C_{i}$ and stem $τ_{i}$ from the statement, and let $λ_{i}^{c w}$ be the loop following $τ_{i}$ , once clockwise around $C_{i}$ , and back. Put $g_{i, j} : = [σ_{j - 1}] \dots [σ_{i + 1}] \in G_{n}$ and let $h_{i, j} = H_{j - 1} \circ \dots \circ H_{i + 1}$ be its mapping-class representative, with the rightmost map acting first. Hence $h_{i, j} (q_{i + 1}) = q_{j}$ and $h_{i, j} (q_{i}) = q_{i}$ . It fixes $C_{i}$ pointwise: each support $U_{r}$ for $r \geq i + 2$ is disjoint from $U_{i}$ , while every point of $C_{i}$ is at distance at least $3 h_{n} - ϵ_{i} \geq 2.9 h_{n} > 3 h_{n} / 2$ from the center of $U_{i + 1}$ . Thus $h_{i, j} \circ τ_{i}$ is a stem from $q_{j}$ to $C_{i}$ , and $h_{i, j} \circ λ_{i}^{c w} = γ_{i, j}^{c w}$ . The path avoids all punctures other than its basepoint because $h_{i, j}$ permutes $Q$ and sends the omitted point $q_{i + 1}$ to $q_{j}$ . The word identity [F3], first-under-second product, and the local winding and typed naturality in [F11] now give $Θ_{n} (A_{i j}) = Ψ_{n}^{m c} ([W_{i j}]) = h_{i, j} Ψ_{n}^{m c} ([σ_{i}^{2}]) h_{i, j}^{- 1} = h_{i, j} {Push}_{q_{i + 1}} ([λ_{i}^{c w}]) h_{i, j}^{- 1} = {Push}_{q_{j}} ([γ_{i, j}^{c w}]) .$ For $j = i + 1$ , $h_{i, j}$ is the identity and this is exactly the local winding case. [F3, F7, F11]

2.3step 1.1F3F4F5F7F11

The conjugated geometric generator has the point-push image along the transported standard stem.

Point-push claim for every pair. By step 2.2, the image under $Θ_{n}$ of the one-coordinate motion along $γ_{i, j}^{c w}$ is ${Push}_{q_{j}} ([γ_{i, j}^{c w}])$ . By step 2.3, this equals $Θ_{n} (A_{i j})$ . Since $Θ_{n}$ is an isomorphism by [F9], it is injective, and therefore $A_{i j} = ι_{*}^{F} [M_{j} (γ_{i, j}^{c w})] .$ This proves claim 1 without an isotopy assertion about the full word motion. [F9, step 2.2, step 2.3]

3.1F9step 2.2step 2.3

Equality under $Θ_{n}$ proves the point-push statement for every pair.

Relabeled form and open-to-closed maps. Let $M_{n}^{ρ} (γ) = (q_{1}, \dots, q_{j - 1}, q_{j + 1}, \dots, q_{n}, γ)$ be the open ordered loop based at $Q^{ρ}$ . Pointwise, $R^{\circ} \circ M_{j} (γ) = M_{n}^{ρ} (γ)$ . The coordinate-permutation square commutes with the open-to-closed inclusions, so $R_{*}^{D} (ι_{*}^{F} [M_{j} (γ)]) = ι_{*}^{F, ρ} [M_{n}^{ρ} (γ)] = κ^{ρ} ([γ]) .$ Apply this identity to the loop from the point-push claim to obtain $R_{*}^{D} (A_{i j}) = κ^{ρ} ([γ_{i, j}^{c w}]) .$ This is the relabeled terminal-coordinate form. The argument uses functoriality only and asserts no injectivity of ${\tilde{κ}}^{ρ}$ or $κ^{ρ}$ . [F6, F10, step 3.1]

4.1F6F10step 3.1

The coordinate permutation carries the proven open motion to the stated closed-disc terminal-coordinate class.

Terminal mapping-class sign. For $i < n$ , the fibre formula and [F9] give $Θ_{n} (A_{i n}) = Θ_{n} (κ_{*} [λ_{i}^{c w}]) = {Push}_{n} ([λ_{i}^{c w}]) .$ The source formula [F2] identifies the configuration-group image of $[W_{i n}]$ as $(κ_{*} [λ_{i}^{c c w}])^{- 1}$ , while [F3] identifies the same image as $(ι_{*}^{F} [z_{W_{i n}}])^{- 1}$ for the raw ordered coordinate loop. Equating and inverting gives $ι_{*}^{F} [z_{W_{i n}}] = κ_{*} [λ_{i}^{c c w}]$ : the raw ordered slice is counterclockwise in the fibre. The configuration identification inverts it, so $A_{i n} = κ_{*} [λ_{i}^{c w}]$ . The inverse-endpoint convention then gives exactly the clockwise point push. [F2, F3, F8, F9, step 2.1]

5.1F2F3F8F9step 2.1∎

This proves the terminal mapping-class sign in claim 3 with the positive generator clockwise.

Remarks

The stem for $A_{i j}$ is the image of the adjacent local stem under the actual mapping-class representative $H_{j - 1} \circ \dots \circ H_{i + 1}$ . This specifies the compatible meridian path and preserves its clockwise orientation.
The relabeling is a coordinate-permutation homeomorphism from basepoint $Q$ to $Q^{ρ}$ . The open terminal-coordinate map and its closed-disc composite have distinct codomains; only the latter is denoted $κ^{ρ}$ in the statement.
The example identifies standard generators and makes no new generation or presentation claim. The proof uses the local two-point winding and typed point-push conjugation already proved in The $A_{i n}$ are meridian generators of the forgetful free kernel.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

118 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

Joan S. Birman and Tara E. Brendle, Braids: A Survey, section 1.2, author manuscript pp. 4-5 (the elementary braid sigma_{s,t} and the pure generators A_{s,t}=sigma_{s,t}^2) (standard reference, not scraped)
Juan Gonzalez-Meneses, Basic results on braid groups, section 2.1, printed pp. 11-14 (Artin words of the pure generators, meridian description of the free kernel) (standard reference, not scraped)
Benson Farb and Dan Margalit, A Primer on Mapping Class Groups, version 5.0 author draft, sections 4.2.1-4.2.3, printed pp. 101-105 (point pushing) (standard reference, not scraped)

Standard AijAij​ as point pushes after relabeling