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.

A maximal torus and Weyl group of SO(3)

Example

Assume the Axiom of Choice. Rotations about a fixed axis form a maximal torus $S O (2) \leq S O (3)$ , and the Weyl group of $S O (3)$ with respect to it has order two, acting on the torus by reversing the angle.

Facts & Assumptions

Given: The group $S O (3)$ of rotations of $R^{3}$ , the subgroup $T$ of rotations about the $z$ -axis, and the half-turn $s$ about the $x$ -axis.

[L1]

$T ≅ S O (2)$ is a compact connected abelian Lie group, hence a torus, and the Weyl group is $W (G, T) = N_{G} (T) / T$ (Tori and maximal tori, Compact Weyl group).

[L2]

Every element of $S O (3)$ is a rotation about some axis through the origin (Euler's theorem for $S O (3)$ ), and the fixed-point set of a nonidentity rotation is its axis. [L1]

Verification

technique · direct

1.1

$T$ is a torus by [L1]. If a connected abelian subgroup $S \supseteq T$ existed, then every element of $S$ would commute with every rotation about the $z$ -axis, and a rotation commuting with all of them fixes the $z$ -axis, hence is itself a rotation about the $z$ -axis; so $S = T$ and $T$ is maximal.

2.1

The half-turn $s$ about the $x$ -axis satisfies $s t s^{- 1} = t^{- 1}$ for $t \in T$ : conjugating a rotation about the $z$ -axis by $s$ reverses its angle, so $s \in N_{G} (T)$ and its class in $W$ is nontrivial.

L1step 1.1

3.1

Conversely, if $g \in N_{G} (T)$ normalizes $T$ , then $g$ preserves the axis of every nonidentity element of $T$ , namely the $z$ -axis as an unoriented line; hence $g$ either preserves or reverses the direction of the $z$ -axis, and modulo $T$ the only two possibilities are the identity and the half-turn's coset.

L1step 2.1

4.1

Therefore $N_{G} (T) / T ≅ Z / 2$ , the nontrivial element acting by $t \mapsto t^{- 1}$ , i.e. by angle reversal; this agrees with the root-system computation for type $A_{1}$ with one positive root.

L1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 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

Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)