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.
All skips and the cone walls of the sortable element s1s2 in A3
Statement
Let be of type , , and . Put for its cover reflections, with the positive-root set of The weak parabolic projection, its adjoints, and the cover-join lemmas (4). Then is -sortable, its sorting word is at positions of the first block of , and its block sequence is the single subset . (i) The leftmost unselected occurrences are at position , at position and at position ; each skip has , so the associated reflections are , and . The words and are reduced while is not, so the skips of and are unforced and the skip of is forced. (ii) Hence the skip roots are These three vectors form a basis of , and . In agreement with Skip roots form a basis, negative skips are cover roots, and the cover decomposition of sortable elements (3), the only element covered by in the weak order is , so , whose positive root is . (iii) The cone is and for every the translate satisfies the three inequalities, because of the adjoint identity together with , , : explicitly , and . Thus , in agreement with the cone criterion at .
Facts & Assumptions
Given: of type with , , , the Coxeter form with , , , the reflection representation , the Coxeter element , and .
The real Coxeter form, its radical, reflections, and form-preserving maps (2): in the type- normalization for all , and .
Coxeter elements, the oriented Euler form, the skew form, and the periodic word (1),(3): for , for and for ; has dividers after each block of letters and the sorting word is the leftmost reduced subword.
c-sortable elements, forced and unforced skips, skip roots, and the chamber cone (1),(2),(3),(4): the definitions of the sorting word, the skips, the associated reflection , forced and unforced skips, the skip roots , the sets and the cone .
The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (1): the greedy scan selects a position with letter exactly when is a left descent of the current remainder and stops at the identity.
Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1),(4): the support of is independent of the reduced expression, and in type the assignment extends to an isomorphism ; under it the length equals the inversion number of the corresponding permutation.
The weak parabolic projection, its adjoints, and the cover-join lemmas (4): the cover roots of are the roots with and for some .
Skip roots form a basis, negative skips are cover roots, and the cover decomposition of sortable elements (1),(2),(3): skip roots are with sign governed by forcedness, the skip set is a basis, and .
The cone criterion, monotonicity of the projection, and the greatest sortable element below w (1): for -sortable with one has .
Descent of the reflection representation, unit root norms, and conjugation of reflections (2): is -preserving, so for all and .
Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the presentation has the relators for and for with ; in particular and .
Proof
The element has and [F5]. The greedy scan of reads the remainders : position has letter and is selected, position has letter and is selected, and position has letter — the scan stops because the remainder is already after two selections [F4]. Hence the sorting word is at positions and the block sequence is the single subset , which is weakly decreasing; so is -sortable [F3].
The selected positions are , so the leftmost unselected occurrences are at position and at positions ; each follows exactly selected letters, so all three skips occur in the rd position of the sorting word [F3].
The associated reflections are , and [F3]; the reductions use for the first and for the second [F10]. The words and are reduced while is not [F5]; hence the skips of and are unforced and the skip of is forced [F3].
The skip roots are , and : the images are computed from [F1] and [F11] as , , , , and , with the sign of the -skip negative because that skip is forced [F3].
The three vectors , and form a basis of : in the basis they are , and , and the last has a nonzero third coordinate while the first two are independent. By [F3] and step 4.1, and .
Cover reflections: the right descents of are read off the products , , ; their lengths are , and [F5], so the only cover relation has and cover reflection , with positive root [F6, F11, step 4.1]. This matches [F7]: the unique negative skip root of is and .
Cone and a chamber check: by [F3] the cone is . For , i.e. for , the adjoint identity [F9] and the inverse images , , [F11, step 4.1] give , and ; hence , that is . This is the instance of the cone criterion at [F8], consistent with being -sortable [step 1.1].
Depends on
- The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment
- c-sortable elements, forced and unforced skips, skip roots, and the chamber cone
- Skip roots form a basis, negative skips are cover roots, and the cover decomposition of sortable elements
- The cone criterion, monotonicity of the projection, and the greatest sortable element below w
- Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification
- Coxeter elements, the oriented Euler form, the skew form, and the periodic word
- The real Coxeter form, its radical, reflections, and form-preserving maps
- The canonical reflection homomorphism, roots, reflections, and the positive cone
- Descent of the reflection representation, unit root norms, and conjugation of reflections
- Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups
- The weak parabolic projection, its adjoints, and the cover-join lemmas
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
79 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
- N. Reading and D. E. Speyer, Sortable elements in infinite Coxeter groups, arXiv:0803.2722v3 (2010); Trans. Amer. Math. Soc. 363 (2011) 699-761 (standard reference, not scraped)
- N. Reading, Sortable elements and Cambrian lattices, arXiv:math/0512339v1 (2005); Algebra Universalis 56 (2007) 35-56 (standard reference, not scraped)
- A. Bjorner and F. Brenti, Combinatorics of Coxeter Groups, Graduate Texts in Mathematics 231, Springer 2005 (standard reference, not scraped)