TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Ordered planar configuration spaces are aspherical

Statement

Assume the Axiom of Choice. For every $n \geq 1$ , every $k \geq 2$ and every base configuration $q \in F_{n} (int D^{2})$ one has $π_{k} (F_{n} (int D^{2}), q) = 0.$ The same conclusion holds for $F_{n} (C)$ and for $F_{n} (D^{2})$ under the coordinatewise radial homeomorphism $C \to int D^{2}$ and the published inclusion homotopy equivalence. Consequently the open-disc and plane ordered configuration spaces are $K (P B_{n}, 1)$ in the higher-homotopy sense: their fundamental group is $P B_{n}$ in the convention of The pure braid group $P B_{n}$ as the fundamental group of an ordered configuration space and all higher homotopy groups vanish.

Facts & Assumptions

Given: the Axiom of Choice, an integer $n \geq 1$ , a base configuration $q = (q_{1}, \dots, q_{n}) \in F_{n} (int D^{2})$ , and the fibre spaces $M_{n - 1} : = int D^{2} ∖ {q_{1}, \dots, q_{n - 1}}$ for $n \geq 2$ .

[A1]

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

[F1]

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

[F2]

For $M = int D^{2}$ and $n \geq 2$ the last-coordinate map $p : F_{n} (int D^{2}) \to F_{n - 1} (int D^{2})$ is, under AC and DC, a numerable locally trivial bundle with fibre over $q^{'}$ equal to $F_{1} (M ∖ Q_{q^{'}}) = M ∖ Q_{q^{'}}$ , hence a Hurewicz and therefore Serre fibration (The Fadell-Neuwirth forgetful map: local triviality, constant fibre, and numerability for configurations in the disk).

[F3]

For a based Serre fibration $p : (E, e_{0}) \to (B, b_{0})$ with fibre $F = p^{- 1} (b_{0})$ the long exact sequence is exact wherever there is an incoming and outgoing arrow; in particular the segment $π_{k} (F) \overset{i_{*}}{\to} π_{k} (E) \overset{p_{*}}{\to} π_{k} (B) \overset{\partial_{p}}{\to} π_{k - 1} (F)$ is exact for every $k \geq 1$ (Long exact sequence of homotopy groups of a fibration).

[F4]

For every finite set $Q$ of distinct points of $int D^{2}$ the complement $int D^{2} ∖ Q$ has $π_{j} = 0$ for every $j \geq 2$ , and $int D^{2}$ itself is contractible; under the explicit radial homeomorphism the same holds for $C$ minus finitely many points (A finitely punctured open disk has the homotopy type of a finite wedge of circles).

[F5]

For every $m \geq 1$ and every base configuration $c \in F_{m} (int D^{2})$ one has $π_{2} (F_{m} (int D^{2}), c) = 0$ (Vanishing $π_{2}$ for every ordered planar configuration space).

[F6]

The inclusion $ι^{F} : F_{m} (int D^{2}) \to F_{m} (D^{2})$ is a homotopy equivalence inducing isomorphisms on all homotopy groups, and the coordinatewise radial map restricts to a homeomorphism $F_{m} (C) \to F_{m} (int D^{2})$ ; homotopy equivalences induce isomorphisms on all $π_{k}$ , $k \geq 1$ , and based homotopy equivalences may be used to transfer vanishing statements (The interior-disc and closed-disc configuration spaces are homotopy equivalent, Higher homotopy basepoint transport and moving homotopies).

[F7]

$P B_{m} = π_{1} (F_{m} (D^{2}), c) = π_{1} (F_{m} (int D^{2}), c)$ for a base configuration $c$ of interior points, by the definition and its displayed inclusion isomorphism (The pure braid group $P B_{n}$ as the fundamental group of an ordered configuration space).

Proof

technique · induction on $n$ for fixed degree $k\ge3$

1.1F4

Fibre degree vanishing. Let $Q$ be any finite set of distinct points of $int D^{2}$ . By [F4] the complement $int D^{2} ∖ Q$ has $π_{j} = 0$ for every $j \geq 2$ ; in particular, for every $k \geq 3$ , both groups $π_{k} (int D^{2} ∖ Q)$ and $π_{k - 1} (int D^{2} ∖ Q)$ vanish.

1.2A1F1F2

The forgetful fibration. By [F1] the Axiom of Choice [A1] yields DC, so for $n \geq 2$ the map $p : F_{n} (int D^{2}) \to F_{n - 1} (int D^{2})$ forgetting the last coordinate is a Hurewicz fibration with fibre $M_{n - 1}$ over $q^{'}$ , by [F2]; the fibre contains $q$ because $q_{n} \neq q_{i}$ for $i < n$ .

1.3baseF4

Base case $n = 1$ . For $n = 1$ single-coordinate evaluation gives $F_{1} (int D^{2}) ≅ int D^{2}$ , which is contractible by [F4]; a contractible space has vanishing $π_{k}$ for every $k \geq 1$ , so $π_{k} (F_{1} (int D^{2}), q) = 0$ for every $k \geq 3$ and every base configuration $q$ .

1.4ih

Induction hypothesis. Fix $k \geq 3$ , fix $n \geq 2$ and assume that $π_{k} (F_{n - 1} (int D^{2}), c) = 0$ for every base configuration $c \in F_{n - 1} (int D^{2})$ .

1.5F5

Degree two. For every $m \geq 1$ and every base configuration $c \in F_{m} (int D^{2})$ one has $π_{2} (F_{m} (int D^{2}), c) = 0$ by [F5]; this is the case $k = 2$ and needs no induction.

1.6F6

Transferring vanishing. By [F6] the coordinatewise radial homeomorphism gives a homeomorphism $F_{m} (C) ≅ F_{m} (int D^{2})$ for every $m$ , and the inclusion $F_{m} (int D^{2}) \to F_{m} (D^{2})$ is a homotopy equivalence; both induce isomorphisms on all $π_{k}$ with $k \geq 1$ , so a vanishing statement transfers across them at corresponding basepoints.

2.1step 1.1step 1.2step 1.4F3

The induction step. Fix $k \geq 3$ , let $q \in F_{n} (int D^{2})$ be an arbitrary base configuration with $n \geq 2$ and put $q^{'} : = (q_{1}, \dots, q_{n - 1})$ . By step 1.2 the map $p$ is a based Serre fibration with $e_{0} = q$ , $b_{0} = q^{'}$ and fibre $M_{n - 1}$ , so the exact segment $π_{k} (M_{n - 1}) \overset{i_{*}}{\to} π_{k} (F_{n} (int D^{2}), q) \overset{p_{*}}{\to} π_{k} (F_{n - 1} (int D^{2}), q^{'}) \overset{\partial}{\to} π_{k - 1} (M_{n - 1})$ of [F3] is available; the outer terms $π_{k} (M_{n - 1})$ and $π_{k - 1} (M_{n - 1})$ vanish by step 1.1, since $k \geq 3$ and $k - 1 \geq 2$ , and $π_{k} (F_{n - 1} (int D^{2}), q^{'}) = 0$ by the induction hypothesis of step 1.4. Exactness then gives $im (i_{*}) = \ker (p_{*}) = 0$ and $im (p_{*}) = \ker (\partial) = 0$ , so $p_{*}$ is both injective and zero and therefore $π_{k} (F_{n} (int D^{2}), q) = 0$ .

3.1step 1.3step 2.1discharge-induction

Induction conclusion. Step 1.3 is the base case and step 2.1 proves the successor implication for arbitrary $n \geq 2$ and arbitrary base configuration, so for every fixed $k \geq 3$ and every $n \geq 1$ one has $π_{k} (F_{n} (int D^{2}), q) = 0$ .

4.1step 1.5step 1.6step 3.1F7discharge-induction

All degrees and all models. Combining step 3.1 with step 1.5 covers every $k \geq 2$ and every base configuration in the open-disc model; applying step 1.6 gives the same vanishing for $F_{n} (C)$ and $F_{n} (D^{2})$ , and [F7] identifies the fundamental group of the open-disc and plane models with $P B_{n}$ , so these spaces are $K (P B_{n}, 1)$ in the higher-homotopy sense.

The induction is on the number of strands for each fixed degree $k \geq 3$ ; the case $k = 2$ was proved separately in advance and is not derived from any point-pushing statement. ∎

Depends on

Used by

Unordered planar configuration spaces are aspherical Corollary

Dependency tree · two levels

69 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 2.1, printed pp. 11-14 (Theorem 2.2: configuration spaces are K(pi,1)) (standard reference, not scraped)
Edward Fadell and Lee Neuwirth, Configuration Spaces, section III, printed pp. 114-115 (standard reference, not scraped)