ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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 Weyl group of A_n is the symmetric group

Example

For $n \geq 1$ , $W (A_{n}) ≅ S_{n + 1}$ , acting on the sum-zero subspace of $R^{n + 1}$ by permuting coordinates.

Facts & Assumptions

Given: An integer $n \geq 1$ , the sum-zero subspace $E \subseteq R^{n + 1}$ , and the model $A_{n} = {ε_{i} - ε_{j} : i \neq j} \subseteq E$ .

[L1]

The coordinate model of $A_{n}$ consists of the roots $ε_{i} - ε_{j}$ in the sum-zero subspace (Classical root systems in coordinates).

[L2]

The Weyl group is generated by the root reflections (Weyl group).

Verification

technique · direct

1.1

Let $ρ : S_{n + 1} \to O (E)$ be the homomorphism obtained by restricting coordinate permutations to $E$ . For $x \in E$ , the reflection formula gives $s_{ε_{i} - ε_{j}} (x) = x - (x_{i} - x_{j}) (ε_{i} - ε_{j}) = ρ ((i j)) x$ . Hence [L2] and the fact that the transpositions generate $S_{n + 1}$ give $W (A_{n}) = ρ (S_{n + 1})$ .

L1L2algebra

2.1

The homomorphism $ρ$ is injective. Indeed, if $ρ (σ)$ is the identity on $E$ , then for every $i \neq j$ it fixes $ε_{i} - ε_{j}$ , so $ε_{σ (i)} - ε_{σ (j)} = ε_{i} - ε_{j}$ ; uniqueness of the positive and negative coordinate positions gives $σ (i) = i$ and $σ (j) = j$ . Thus $σ = 1$ , and step 1.1 yields $W (A_{n}) ≅ S_{n + 1}$ with the asserted action.

L1step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I, Lectures 19-24 (standard reference, not scraped)