CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

Collisions destroy freeness of the coordinate permutation action

Statement refuted

The following over-generalisation is false. Let $n \geq 2$ , let $X$ be a nonempty topological space, and let $S_{n}$ act on the full product $X^{n} = \prod_{k < n} X$ (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space) by the coordinate permutation formula

$(σ \cdot x)_{i} : = x_{σ^{- 1} (i - 1) + 1} (1 \leq i \leq n),$

the formula by which $S_{n}$ acts on the collision-free subspace $F_{n} (X) \subseteq X^{n}$ (The symmetric group acts continuously and freely on $F_{n} (X)$ by permuting labels). Refuted claim: this action on $X^{n}$ is free (A free group action has no nonidentity element fixing a point). It is not: for $n \geq 2$ and every nonempty $X$ some nonidentity permutation fixes a tuple whose coordinates are not pairwise distinct, whereas the restricted action on $F_{n} (X)$ is free precisely because collisions have been removed. No claim is made here about the boundary cases $n \leq 1$ , where $S_{n}$ is trivial and the action is free for trivial reasons.

Facts & Assumptions

Given: A natural number $n \geq 2$ , a nonempty topological space $X$ , the product $X^{n}$ with the product topology, and an element $x \in X$ .

[F1]

For $n \in N$ the product $X^{n} = \prod_{k < n} X$ has as its points the functions $n \to X$ , displayed as tuples $(x_{1}, \dots, x_{n})$ where the label $i$ names the coordinate of index $i - 1$ ; the collision-free subspace is $F_{n} (X) = {(x_{1}, \dots, x_{n}) \in X^{n} : x_{i} \neq x_{j} for i \neq j}$ , and for $X^{n}$ no distinctness is required (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Ordered configuration spaces $F_{n} (X)$ ).

[F2]

$S_{n} = Sym (n)$ is a group under composition with $(σ τ) (k) = σ (τ (k))$ for $k \in n$ and $(σ τ)^{- 1} = τ^{- 1} σ^{- 1}$ , and the formula $(σ \cdot x)_{i} = x_{σ^{- 1} (i - 1) + 1}$ defines a continuous free left action of $S_{n}$ on $F_{n} (X)$ ; in particular $σ \cdot x = x$ for $x \in F_{n} (X)$ forces $σ = id$ ( $Sym (X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements, The finite symmetric group $S_{n}$ , one-line notation, and cycle notation, Left group actions, transitive actions, and faithful actions, A free group action has no nonidentity element fixing a point, The symmetric group acts continuously and freely on $F_{n} (X)$ by permuting labels).

[F3]

For $n \geq 2$ the symmetric group $S_{n}$ contains nonidentity elements: the transposition $τ$ defined by $τ (0) = 1$ , $τ (1) = 0$ and $τ (k) = k$ for $k \in n ∖ {0, 1}$ satisfies $τ \neq id$ , and cycle notation records it as $(0 1)$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation, $Sym (X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements).

[F4]

A left action is free when $g \cdot x = x$ implies $g = e$ ; a single tuple with a nonidentity stabiliser therefore refutes freeness (A free group action has no nonidentity element fixing a point, Left group actions, transitive actions, and faithful actions). Nonemptiness of $X$ means exactly that some element $x \in X$ exists, and exhibiting one element requires no choice principle.

[F5]

Two elements of a product are equal exactly when they agree in every coordinate; the constant tuple $(x, \dots, x) \in X^{n}$ has all its coordinates equal to $x$ (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

Refutation

technique · direct

1.1

The formula defines a left action on the whole product. For $σ \in S_{n}$ and $y \in X^{n}$ the tuple $σ \cdot y$ with $(σ \cdot y)_{i} = y_{σ^{- 1} (i - 1) + 1}$ is well defined in $X^{n}$ , because $σ^{- 1} (i - 1) + 1$ is a label for every $i$ by [F2]; and the formal verification of $id \cdot y = y$ and $(σ τ) \cdot y = σ \cdot (τ \cdot y)$ for $σ, τ \in S_{n}$ is the reindexing computation of [F2], which never uses the distinctness of coordinates, so it applies to all of $X^{n}$ . Hence [F3] and [F4] apply to this action.

F1F2

1.2

The collision witness. Fix an element $x \in X$ , which exists by [F4], and put $a : = (x, x, \dots, x) \in X^{n}$ , the tuple with $a_{i} = x$ for every label $i$ ; its coordinates collide, and $a \notin F_{n} (X)$ when $n \geq 2$ because $a_{1} = a_{2}$ . So $a$ is a point of $X^{n}$ to which the freeness conclusion of [F2] does not apply.

F1F4F5

2.1

The transposition fixes $a$ . By step 1.1 the tuple $τ \cdot a \in X^{n}$ is defined, and for every label $i$ one has $(τ \cdot a)_{i} = a_{τ^{- 1} (i - 1) + 1} = x = a_{i}$ , because all coordinates of $a$ equal $x$ ; hence $τ \cdot a = a$ by [F5].

step 1.1F2F5

3.1

Freeness fails. The transposition $τ$ is not the identity by [F3], yet it fixes the point $a$ of $X^{n}$ by step 2.1. Therefore the action of $S_{n}$ on $X^{n}$ is not free, in the sense of the definition in [F4].

step 2.1F3F4

4.1

Conclusion. The claim stated in the refuted statement is false for every $n \geq 2$ and every nonempty $X$ , with the explicit witness $a = (x, \dots, x)$ fixed by the transposition $τ = (0 1)$ . The contrast with [F2] is exactly the removal of the collision diagonals: freeness of the coordinate permutation action is a property of $F_{n} (X)$ , not of the full product $X^{n}$ .

step 1.2step 3.1F2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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 González-Meneses, Basic results on braid groups, §§1.1–1.3 and 2.1, printed pp. 3–6, 11–13 (standard reference, not scraped)