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.
Finite Weyl root system, lattice and chamber conventions
Definition
Let be a finite-dimensional real vector space with a positive definite symmetric bilinear form . A finite reduced crystallographic root system is a finite subset spanning , such that for every the integer is integral, the reflection preserves , and the only scalar multiples of in are . The Weyl group is the subgroup of linear isometries of generated by these reflections. A root reflection means one of the . The empty root system on is allowed, with .
Choose such that for every root. Put and . A positive root is simple if it is not the sum of two positive roots. The following positive-root lemma proves that the simple roots form a basis and that the simple reflections generate ; no such assertion is assumed by this definition. Once proved, let be the least number of simple reflections in a word for and let . A word is reduced if its length equals .
Identify with its dual by the displayed form, so . The root and coroot groups are and . The weight group is ; the positive-root lemma proves it is a lattice with basis the vectors dual to the simple coroots. Put , and write when . The open and closed positive chambers are and . A weight is dominant if it belongs to . More generally chambers are the connected components of . The closed-chamber representative and stabilizer assertions are proved later, not included as axioms.
Used by
- Bruhat order on a finite Weyl group Definition
- Weyl discriminant and reflecting hyperplane arrangement Definition
- Weyl orbit sum in a group algebra Definition
- Finite semisimple Cartan, root and string structure Lemma
- Finite Weyl closed chambers and stabilizers Lemma
- Finite Weyl positive roots and simple reflections Lemma
- Finite Weyl strong exchange and deletion Lemma
- Weyl orbit sums form a basis of finite Weyl invariants Lemma
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Pavel Etingof, Lie Groups and Lie Algebras, §§21–22; local sign-change proofs fill the chamber argument (standard reference, not scraped)