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 strong exchange and deletion
Statement
For the simple reflections of a finite reduced crystallographic root system, word length equals inversion length: . If a root reflection satisfies , every reduced word for loses exactly one letter to give . Every nonreduced word admits deletion of two letters without changing its group element.
More precisely, for , if and only if . In this case one letter can be deleted from any word for to give , although the resulting word need not be reduced. Also , with the minus sign exactly when . These are assertions for the geometric reflection group, without an assumed Coxeter presentation or exchange axiom.
Facts & Assumptions
Given: The finite root system, positivity and word conventions.
These conventions are Finite Weyl root system, lattice and chamber conventions.
Simple reflections generate and permute the positive roots other than their own simple root by Finite Weyl positive roots and simple reflections.
Proof
Let be any word, and suppose but . Starting with , apply successively; the resulting final vector is . At the first positive-to-negative change, say index , F2 implies . With this says . The reflection identity therefore cancels precisely the th letter in . This proves the claimed deletion for every word, including an initially nonreduced one.
If , apply step 1.1 to a reduced word to get . If , put ; then , so the same argument gives . These two cases prove the reflection-descent criterion and strong exchange. Reversing a word proves . Applying the criterion to and gives the sign of . Appending or removing a single bounds its absolute value by one, so the difference is exactly .
Write . Since permutes , counting those roots first gives if , and if . To prove , induct on reduced word length. The empty word has both numbers zero. If is reduced, its prefix is reduced, since a shorter prefix would shorten . Step 2.1 gives , as the negative case would make . Thus . This also proves that an element preserving all positive roots is the identity.
Consider a nonreduced word and its first nonreduced prefix , where the given word for is reduced. Step 2.1 forces , so . Apply step 1.1 to the reversed word for and the positive root . It deletes one letter to express . Reverse this equality to express by the word for with that letter deleted. In the original prefix this removes that letter and its terminal , hence two letters without changing its value. Reattach the remaining suffix of the original word. All arguments are finite, include rank zero and the identity, and use no AC.
Depends on
Used by
Dependency tree · one level
2 results within one dependency step 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
- Pavel Etingof, Lie Groups and Lie Algebras, §§21–22; local sign-change proofs fill the chamber argument (standard reference, not scraped)