Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Root reflections preserve the root set

Statement

Assume the Axiom of Choice. Let h be a Cartan subalgebra of a finite-dimensional complex semisimple Lie algebra g with root set Φ (Root and root space). For roots α,βΦ, the reflected functional sα(β) (Root reflection defined by a coroot) is again a root.

Facts & Assumptions

Given: The Axiom of Choice, such g,h and roots α,β.

[A1]

The Axiom of Choice is The Axiom of Choice; it licenses the root-string, coroot, and reflection facts in [L1] and [L2].

[L1]

The set {kZ:gβ+kα0} of indices k with β+kα a root or zero is a nonempty interval {p,,q} of consecutive integers with pq=β(hα) (The root-string property).

[L2]

The reflection is sα(λ)=λλ(hα)α, and β(hα)Z (Root reflection defined by a coroot, Cartan integers are integers, Coroot of a Lie-algebra root).

Proof

technique · direct
1.1

By [L1] applied to the pair (α,β) there are integers p,q0 with pq=β(hα) and such that β+kαΦ{0} for every k with pkq.

A1L1L2
2.1

By [L2] we may rewrite sα(β)=ββ(hα)α=β+(qp)α, and the index k=qp satisfies pqpq because p,q0. Hence sα(β)=β+kα with pkq, so sα(β)Φ{0} by step 1.1.

L1L2step 1.1algebra
3.1

Finally sα(β)0: if β+(qp)α=0 then β is a scalar multiple of α, so sα(β)=0 would mean β=β(hα)α; but then β and α are proportional roots and the reflection of a nonzero functional is nonzero because sα is an involutive linear automorphism of h (Root reflection defined by a coroot) with sα(α)=α0. Hence sα(β)Φ, as claimed.

step 2.1algebra

Depends on

Used by

Dependency tree · two levels

16 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