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 two-sphere as a coadjoint orbit of SO(3)

Example

Identify $s o (3)$ with $R^{3}$ by $v \mapsto (u \mapsto v \times u)$ , so that the bracket becomes the cross product, the adjoint and coadjoint actions become the standard rotation action of $S O (3)$ on $R^{3}$ , and $s o (3)^{*}$ is identified with $R^{3}$ compatibly. Then the coadjoint orbits are the origin and the spheres $S_{r}^{2} = {v : ∣ v ∣ = r}$ of radius $r > 0$ . If $D_{r} : S^{2} \to S_{r}^{2}$ is the dilation $D_{r} (x) = r x$ , then on the sphere the KKS form $ω_{r}$ satisfies

$ω_{r, α} (ξ_{O} (α), η_{O} (α)) = α \cdot (ξ \times η), D_{r}^{*} ω_{r} = r ω_{S^{2}}, ∣ α ∣ = r,$

and the inclusion $S_{r}^{2} ↪ R^{3}$ is an equivariant moment map for the rotation action.

Facts & Assumptions

Given: ${A C}_{ω}$ , the identification of $s o (3)$ and $s o (3)^{*}$ with $R^{3}$ , and a covector $α \neq 0$ .

[F1]

$S O (3)$ is an embedded Lie group with Lie algebra the skew-symmetric matrices $s o (3)$ , and the cross product on $R^{3}$ is given by its coordinate determinant formula (Orthogonal and special orthogonal Lie groups, The cross product in $R^{3}$ ). The adjoint and coadjoint actions have their usual definitions (The coadjoint representation, action and orbits); their concrete rotation formulas for the identification used here are verified in step 1.1.

[F2]

Coadjoint orbits carry the KKS form $ω_{β} (ξ_{O} (β), η_{O} (β)) = β ([ξ, η])$ , which is symplectic and $G$ -invariant, and the orbit inclusion is an equivariant moment map. Coadjoint orbits are symplectic manifolds, The coadjoint-orbit inclusion is an equivariant moment map.

[F3]

The standard oriented area form of the unit sphere is $ω_{S^{2}, \hat{α}} (u, v) = \hat{α} \cdot (u \times v)$ for tangent vectors $u, v$ ; the scalar-triple-product formula makes it rotation invariant. The cross product in $R^{3}$ .

Verification

technique · direct

1.1

For $v = (v_{1}, v_{2}, v_{3})$ put $\hat{v} = (\begin{array}{ccc} 0 & - v_{3} & v_{2} \\ v_{3} & 0 & - v_{1} \\ - v_{2} & v_{1} & 0 \end{array}) .$ Then $\hat{v} u = v \times u$ , and every skew-symmetric $3 \times 3$ matrix is uniquely of this form. Direct multiplication using the coordinate cross-product formula gives $[\hat{v}, \hat{w}] = \hat{v \times w}$ . Moreover, for $R \in S O (3)$ the scalar-triple-product identity and $\det R = 1$ give $R (v \times u) = (R v) \times (R u)$ , so $R \hat{v} R^{- 1} = \hat{R v}$ . Thus the adjoint action is the standard rotation action. Under the dot-product identification $(R^{3})^{*} ≅ R^{3}$ , orthogonality of $R$ then makes the coadjoint action the same rotation action.

F1algebra

2.1

By step 1.1 the coadjoint orbit of $α$ is the set of vectors of the same length, hence the sphere $S_{r}^{2}$ of radius $r = ∣ α ∣$ when $α \neq 0$ , and the origin when $α = 0$ .

step 1.1given

3.1

With the library's negative-exponential convention for fundamental fields, step 1.1 gives $ξ_{O} (α) = α \times ξ$ . The KKS formula [F2] therefore reads $ω_{r, α} (ξ_{O} (α), η_{O} (α)) = α \cdot (ξ \times η)$ . Write $α = r \hat{α}$ . Dilation intertwines the rotation actions, hence $d (D_{r}^{- 1})_{α} ξ_{O} (α) = ξ_{O} (\hat{α})$ and similarly for $η$ . The vector identity $\hat{α} \cdot ((\hat{α} \times ξ) \times (\hat{α} \times η)) = \hat{α} \cdot (ξ \times η)$ and [F3] give $ω_{r, α} (ξ_{O} (α), η_{O} (α)) = r ω_{S^{2}, \hat{α}} (d (D_{r}^{- 1})_{α} ξ_{O} (α), d (D_{r}^{- 1})_{α} η_{O} (α)),$ which is exactly $D_{r}^{*} ω_{r} = r ω_{S^{2}}$ .

step 1.1step 2.1F2F3algebra

4.1

Consequently the total area of the coadjoint orbit $S_{r}^{2}$ is $4 π r$ , and the form is nondegenerate and closed by [F2]; the rotation action is transitive on the sphere and preserves the form, as required of a coadjoint orbit.

step 3.1F2F3

5.1

By [F2] the inclusion $S_{r}^{2} ↪ R^{3}$ is an equivariant moment map for the rotation action with this KKS form; explicitly, for $α$ of length $r$ and $ξ \in R^{3}$ , $d ⟨ Φ, ξ ⟩_{α} (η_{O}) = α \cdot (η \times ξ) = - ω_{α} (ξ_{O}, η_{O})$ , which is the moment equation of the library convention.

step 3.1F2F3∎

Depends on

Used by

The shifting trick for a nonzero coadjoint orbit Example

Dependency tree · two levels

37 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

Eckhard Meinrenken, Symplectic Geometry (standard reference, not scraped)
Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)