LemmaStatement: 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.

Vanishing $π_{2}$ for every ordered planar configuration space

Statement

Assume the Axiom of Choice. For every $n \geq 1$ and every base configuration $q \in F_{n} (int D^{2})$ one has $π_{2} (F_{n} (int D^{2}), q) = 0.$ The same conclusion holds for $F_{n} (C)$ under the coordinatewise radial homeomorphism $C \to int D^{2}$ , $w \mapsto w / (1 + ∣ w ∣)$ , applied to every coordinate, and for $F_{n} (D^{2})$ under the published inclusion homotopy equivalence $F_{n} (int D^{2}) \to F_{n} (D^{2})$ .

Facts & Assumptions

Given: the Axiom of Choice (AC) and, for every $n \geq 1$ , an arbitrary base configuration $q = (q_{1}, \dots, q_{n}) \in F_{n} (int D^{2})$ ; write $M : = int D^{2}$ and $M ∖ {q_{1}, \dots, q_{n - 1}}$ for the complement of the first $n - 1$ coordinates.

[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]

Let $M$ be a nonempty connected Hausdorff topological $d$ -manifold without boundary with $d \geq 2$ and let $m, n \geq 1$ ; the map $π : F_{m + n} (M) \to F_{m} (M)$ , $π (x_{1}, \dots, x_{m + n}) : = (x_{1}, \dots, x_{m})$ , has fibre $π^{- 1} (q^{'}) ≅ F_{n} (M ∖ Q_{q^{'}})$ over every base configuration $q^{'}$ , it is a locally trivial fibre bundle with that fibre type, and if $M = int D^{2}$ then under AC and DC the bundle may be taken numerable and is therefore a Hurewicz 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 segment $π_{2} (F) \overset{i_{*}}{\to} π_{2} (E) \overset{p_{*}}{\to} π_{2} (B) \overset{\partial_{p}}{\to} π_{1} (F)$ of the long exact sequence is exact, exactness meaning that the incoming image equals the inverse image of the distinguished element (Long exact sequence of homotopy groups of a fibration).

[F4]

For every finite set $Q$ of $k$ distinct points of $int D^{2}$ , $π_{j} (int D^{2} ∖ Q) = 0$ for every $j \geq 2$ , and for $k = 0$ the space $int D^{2}$ is contractible; the same conclusions hold for $C$ minus $k$ points under the explicit radial homeomorphism $h (w) = w / (1 + ∣ w ∣)$ (A finitely punctured open disk has the homotopy type of a finite wedge of circles).

[F5]

A based homotopy equivalence $f : (X, x) \to (Y, f (x))$ induces isomorphisms $f_{*} : π_{j} (X, x) \to π_{j} (Y, f (x))$ for all $j \geq 1$ , and the inclusion $ι^{F} : F_{n} (int D^{2}) \to F_{n} (D^{2})$ is a homotopy equivalence with $ι_{*}^{F}$ an isomorphism on fundamental groups at every configuration of interior points (Higher homotopy groups are functorial and based homotopy invariant, The interior-disc and closed-disc configuration spaces are homotopy equivalent).

Proof

technique · induction on $n$

1.1F4

The fibre fact. By [F4], for every finite set $Q$ of distinct points of $int D^{2}$ the complement $int D^{2} ∖ Q$ has vanishing $π_{j}$ in every degree $j \geq 2$ and, when $Q$ is empty, is contractible; in particular every group $π_{2} (int D^{2} ∖ Q)$ is trivial.

1.2F4F5

Transferring the conclusion. The coordinatewise map $h^{(n)} : C^{n} \to (int D^{2})^{n}$ , $h (z_{1}, \dots, z_{n}) = (h (z_{1}), \dots, h (z_{n}))$ , restricts to a homeomorphism $F_{n} (C) \to F_{n} (int D^{2})$ , and the inclusion $ι^{F} : F_{n} (int D^{2}) \to F_{n} (D^{2})$ is a homotopy equivalence; by [F5] both induce isomorphisms on all homotopy groups in degrees $\geq 1$ , so vanishing of $π_{2}$ transfers in either direction and at the corresponding basepoints.

1.3baseF4

Base case $n = 1$ . For $n = 1$ single-coordinate evaluation is a homeomorphism $F_{1} (int D^{2}) ≅ int D^{2}$ , which is the case $k = 0$ of the vanishing statement in [F4], so $π_{2} (F_{1} (int D^{2}), q) = 0$ for the arbitrary base configuration $q$ .

1.4ih

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

1.5A1F1F2

The forgetful fibration. By [F1], the Axiom of Choice [A1] yields the Axiom of Dependent Choice, so the choice hypotheses of [F2] are met; fixing $n \geq 2$ and a base configuration $q$ , the map $p_{n} : F_{n} (int D^{2}) \to F_{n - 1} (int D^{2})$ , $(x_{1}, \dots, x_{n}) \mapsto (x_{1}, \dots, x_{n - 1})$ , is of the form in [F2] with $m = n - 1 \geq 1$ and one forgotten point on the manifold $M = int D^{2}$ , and is therefore a Hurewicz, hence Serre, fibration; over $b : = p_{n} (q) = (q_{1}, \dots, q_{n - 1})$ its fibre is $p_{n}^{- 1} (b) = F_{1} (int D^{2} ∖ {q_{1}, \dots, q_{n - 1}}) = int D^{2} ∖ {q_{1}, \dots, q_{n - 1}}$ , which contains $q$ because $q_{n} \notin {q_{1}, \dots, q_{n - 1}}$ . This use of AC is the only one in the proof, and it is used solely to invoke [F2].

2.1step 1.1step 1.4step 1.5F3

The induction step. Let $q \in F_{n} (int D^{2})$ be arbitrary and let $p_{n}$ , $b = p_{n} (q)$ and the fibre $F = int D^{2} ∖ {q_{1}, \dots, q_{n - 1}}$ be as in step 1.5, so that $q \in F$ . The map $p_{n}$ is a based Serre fibration, so the exact segment $π_{2} (F) \overset{i_{*}}{\to} π_{2} (F_{n} (int D^{2}), q) \overset{p_{n *}}{\to} π_{2} (F_{n - 1} (int D^{2}), b) \overset{\partial}{\to} π_{1} (F)$ of [F3] is available. The term $π_{2} (F)$ is zero by step 1.1, and $π_{2} (F_{n - 1} (int D^{2}), b) = 0$ by the induction hypothesis of step 1.4, so exactness gives $im (i_{*}) = \ker (p_{n *}) = 0$ and $im (p_{n *}) = \ker (\partial) = 0$ ; hence $p_{n *}$ is both injective and zero, and therefore $π_{2} (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 by induction $π_{2} (F_{n} (int D^{2}), q) = 0$ for every $n \geq 1$ and every $q \in F_{n} (int D^{2})$ .

4.1step 3.1step 1.2discharge-induction

The plane and closed-disc models. Applying the homeomorphism and the homotopy equivalence of step 1.2 to the result of step 3.1 gives $π_{2} (F_{n} (C), q^{'}) = 0$ for every $q^{'} \in F_{n} (C)$ and $π_{2} (F_{n} (D^{2}), q^{''}) = 0$ for every $q^{''} \in F_{n} (D^{2})$ , which is the full statement.

∎

Depends on

Used by

Dependency tree · two levels

66 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 (the exact sequences of the pure braid tower and the pi_2 vanishing induction) (standard reference, not scraped)
Edward Fadell and Lee Neuwirth, Configuration Spaces, section II, printed pp. 111-114 and section III, printed pp. 114-115 (standard reference, not scraped)

Vanishing π2π2​ for every ordered planar configuration space