Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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 Levi decomposition of the Euclidean-motion algebra of R^3

Example

The Euclidean-motion algebra of three-space has the Levi decomposition

e(3)=R3so(3),rad(e(3))=R3,

where translations form the radical and rotations form a Levi factor.

Facts & Assumptions

Given: The standard action of so(3) on R3 and the resulting semidirect-product bracket.

[L1]

A Levi decomposition is a vector-space semidirect sum of the radical and a semisimple subalgebra (Levi subalgebras and Levi decompositions).

Verification

technique · direct
1.1

Put V=R3. In the semidirect product, [(v,A),(w,B)]=(AwBv,[A,B]). Hence V0 is an abelian ideal, and the quotient by it is so(3).

givenalgebra
1.2

Under the vector-space identification uAu, Au(v)=u×v, one has [Au,Av]=Au×v. If an ideal of so(3) contains a nonzero Au, then the vectors u×v as v varies span u, and a further bracket supplies the u-direction. Thus the ideal is all of so(3). The algebra is nonabelian and [so(3),so(3)]=so(3), so it is simple and not solvable.

algebra
2.1

Let I be a solvable ideal of e(3). Its image in the quotient is a solvable ideal of so(3), hence is zero by step 1.2. Thus IV. Conversely V is itself a solvable ideal by step 1.1, so it is the radical.

step 1.1step 1.2
3.1

The subalgebra 0so(3) is semisimple, meets V in zero, and together with V spans the whole algebra. It is therefore a Levi factor by [L1]. The zero intersections and full quotient are explicit, and no choice is used.

L1step 1.1step 1.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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