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.
Coxeter Euler Forms and Sortable Chamber Cones — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Canonical Roots, Signs, and Faithful Reflections
- Chains, Antichains, Sperner and Dilworth
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Conjugacy in Sₙ, Generation, and the Simplicity of Aₙ
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Coxeter Euler Forms and Sortable Chamber Cones
- Coxeter Presentations, Exchange, and Reduced Word Theorems
- Cyclic Groups and Direct Products
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Coxeter Diagrams and Complete Classification
- Finite Fields and Cyclotomic Extensions
- Finite Reflection Arrangements and Spherical Coxeter Complexes
- Foundations of the Real Numbers for Analysis
- Free Groups and Presentations
- Further Trigonometric Identities and Inverse Functions
- Graphs, Walks and Connectivity
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Incidence Algebras and Möbius Inversion
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Parabolic Subgroups and Double Coset Geometry
- Partitions of Unity and Paracompactness
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Properties of the Integral and the Working FTC
- Real Forms and Reflection Geometry
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Simplicial Complexes and Simplicial Homology
- Sine, Cosine, and the Definition of Pi
- Splitting Fields
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Fundamental Theorem of Finite Abelian Groups
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The ZFC Axioms and the Basic Set Constructions
- Tits Cones, Chambers, and Parabolic Stabilizers
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Order, Inversions, and Lattice Operations
2 · Summary
This draft companion is a dependency leaf. Its exercises and examples use only the theory of coxeter-euler-forms-and-sortable-chamber-cones and that page’s established prerequisite closure; no other theory page may depend on a supplier homed here.
For c=s1s2s3 in A3 compute the Euler/skew form, all skips of a short sorting word and cone walls. Change c by a source-sink move and check the sign convention. Test a rank-two inversion set violating closure.
Each example states its hypotheses and checks the calculation directly. A counterexample identifies the precise dropped hypothesis; a drawing or symbolic calculation alone does not certify a general theorem.
A2 rank-two inversion-set counterexample
A set of two reflections of A2 that fails both closure and the segment criterion lists every inversion set in A2 and shows that positive-combination closure alone does not recognize inversion sets.
Euler and skew forms in A3
The Euler and skew forms of c = s1s2s3 in A3, and the orientation of its rank-two subsystems computes the Euler and skew forms for , checks their signs on the two standard A2 root orders, and recomputes the forms for .
A source–sink move and the sign convention
A source–sink move in A3: transporting the Euler and skew forms by an initial letter conjugates by the initial letter , recomputes and for the reduced Coxeter word , and verifies on all nine basis pairs that the forms transport by while the sign of the noncommuting pair is prescribed by the order of its letters in the word.
Skips and cone walls for a short sorting word
All skips and the cone walls of the sortable element s1s2 in A3 computes all skips, skip roots, forced and unforced alternatives of the -sortable element in , identifies the unique cover reflection of , and verifies the cone inclusion predicted by the cone criterion.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A set of two reflections of A2 that fails both closure and the segment criterion
Statement
Let be the Coxeter system of type , with and . Its reflections and corresponding positive roots in angular order are (Plane subsystems, their canonical generators, and the angular order of their roots (2), The real Coxeter form, its radical, reflections, and form-preserving maps (2), The inversion formula , the root-reflection dictionary and strong exchange (1)). Put
(i) is not for any ; explicitly,
(ii) A set is closed under positive rank-two combinations when it contains every root with and in the set. Then is not closed: it contains but omits their root . Its complement is closed.
(iii) is neither an initial nor a final segment of . Thus the rank-two segment criterion of Finite inversion sets are recognized by their rank-two initial or final segments (1)(ii) rejects .
(iv) By contrast, is the initial segment and equals .
(v) The complement is closed under positive rank-two combinations but is not an inversion set. Thus closure of a set alone is insufficient.
Facts & Assumptions
Given: The type- Coxeter system, its canonical real reflection representation, the positive roots and angular order in the Statement, and the inversion-set map .
For a two-dimensional root plane with , the canonical angular list has three positive roots (Plane subsystems, their canonical generators, and the angular order of their roots (2)); the extreme-root rays here are and .
The reflection subgroup is dihedral of order (Plane subsystems, their canonical generators, and the angular order of their roots (3)); in this rank-two ambient system and the face point is , so that subgroup is .
A finite positive-root set is an inversion set exactly when its restriction to every noncommutative generalized rank-two subsystem is empty, an initial segment, or a final segment (Finite inversion sets are recognized by their rank-two initial or final segments (1)).
For a root , , and the positive roots are in bijection with reflections (The inversion formula , the root-reflection dictionary and strong exchange (1)).
Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the type- presentation has .
Proof
Finite setup and root order. From [F8], ; canceling equal adjacent letters and replacing by and by reduces every word to one of . Hence is finite and the finite-type suppliers [F1],[F2] apply. Since , [F3, F4] give , , , and ; by linearity and . The orbit definition makes a positive root, and [F1] gives exactly three positive roots in the plane. The extreme rays of are generated by , so their angular order is . By [F7], , while and ; hence the reflection order is .
Closure. The roots belong to , and their positive combination is a root missing from , so is not closed. The complement contains only ; the positive-root list has no other root on that ray, so every positive combination of two complement members that is a root is again . Hence the complement is closed.
Exhaustive inversion-set calculation. The rank-two presentation gives the six normal forms for by [F2]. Applying step 1.1 with the rightmost generator acting first, the images of under those elements are , , , , , and , respectively. By [F5], their inversion sets are , , , , , and . These six elements exhaust by [F2], and none of these sets is .
Segment criterion. In the order , the initial segments are and the final segments are . The set is neither. By [F6] it fails the rank-two criterion, agreeing with the exhaustive calculation in step 2.1.
A valid two-root segment. Step 2.1 gives , the initial segment consisting of the first two roots in the displayed order.
The closed non-inversion set. Step 1.2 proves that is closed, and the exhaustive list in step 2.1 contains no such singleton inversion set. This proves (v).
Conclusion. Steps 1.1-3.3 establish (i)-(v) by finite matrix and set calculations. No witness is selected from an infinite family, so AC is not used.
The Euler and skew forms of c = s1s2s3 in A3, and the orientation of its rank-two subsystems
Statement
Let have type , with , , and . Put ; it is a reduced Coxeter word by Coxeter words are commutation-connected; the Euler and skew forms depend only on the Coxeter element (1). With respect to the simple basis , the Cartan form and the forms of Coxeter elements, the oriented Euler form, the skew form, and the periodic word are
(i) , and is lower triangular with diagonal , as specified by the ordered word .
(ii) The sign table is , , and . Thus the commuting pair has zero orientation and each adjacent pair is positive in the order induced by .
(iii) Put , , , and . By The inversion formula , the root-reflection dictionary and strong exchange and Plane subsystems, their canonical generators, and the angular order of their roots, these are the generalized rank-two parabolics attached to and . The positive roots in the displayed planes, in angular order from the ray of to that of and from to , are and , respectively. For each , on this root order is positive on all pairs in increasing order. For each subgroup, the restrictions , for , are exactly the empty, initial, and final segments; these are the rank-two patterns in Finite inversion sets are recognized by their rank-two initial or final segments (1).
(iv) For the other Coxeter word , Thus while : the orientation of the edge is reversed and the commuting pair still has value . No Axiom of Choice is used.
Facts & Assumptions
Given: The type- Coxeter matrix, its simple basis, real reflection representation and positive roots, and the two ordered words and .
For the type- matrix, the canonical map to is an isomorphism (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4)).
Every standard parabolic is a Coxeter system with the restricted matrix (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2)).
Finite type (spherical type) means exactly that is finite (Coxeter diagrams: edges, labels, components and finite type (4)).
A Coxeter word uses each element of once (Coxeter elements, the oriented Euler form, the skew form, and the periodic word (1)).
Every Coxeter word is reduced (Coxeter words are commutation-connected; the Euler and skew forms depend only on the Coxeter element (1)).
For the chosen ordered word, and when , when , and when ; (Coxeter elements, the oriented Euler form, the skew form, and the periodic word (2)).
and for finite (The real Coxeter form, its radical, reflections, and form-preserving maps (2)).
For a root , its associated reflection is ; in particular, (The inversion formula , the root-reflection dictionary and strong exchange (1)).
For every root-spanned plane , there is an such that for every root ; for such the rank-two subgroup satisfies (Plane subsystems, their canonical generators, and the angular order of their roots (1)).
If are the extreme positive roots in and , then is dihedral (Plane subsystems, their canonical generators, and the angular order of their roots (2),(3)).
The reflection with normal is (The real Coxeter form, its radical, reflections, and form-preserving maps (3)).
is a homomorphism with (The canonical reflection homomorphism, roots, reflections, and the positive cone (1)).
, where is the cone of nonnegative simple coordinates; every root is positive or negative (Root sign coherence and the action of simple reflections on positive roots (2)).
A finite positive-root set is an inversion set exactly when every noncommutative generalized rank-two restriction is empty, an initial segment, or a final segment (Finite inversion sets are recognized by their rank-two initial or final segments (1)).
Proof
Finite-type setup. By [F1], is isomorphic to and hence finite; by [F3] it is of finite type. Each displayed word uses every simple generator once by [F4], so [F5] says that and are reduced Coxeter words, as required to define their Euler forms.
Cartan and Euler matrices. From [F7], , , and . Applying [F6] in the order gives exactly the displayed ; subtracting its transpose gives the displayed . For , , so is positive definite.
The second Coxeter word. The word uses each generator once by [F4] and is reduced by [F5]. With its order , [F6]-[F7] give the displayed and matrices. Their entries yield , , and , proving (iv).
The two rank-two root lists. Let be the standard basis of and let . The vectors have Gram matrix from step 1.2, so extends to an isometry from to . Under it, [F11]-[F12] identify with the coordinate transposition . Since the adjacent transpositions generate and [F1] identifies with , the root orbit [F13] is exactly . The positive members are exactly those with , whose simple coordinates are , by [F14]. In each rank-two plane the three positive roots have coefficient pairs in its simple basis, so the middle root lies strictly inside the sector from the first simple root to the second. Thus the positive roots in and are exactly the three displayed in (iii), in the stated angular orders.
Symmetrization and simple-root signs. Adding the displayed matrices yields . The entries of give , , and .
All rank-two signs. By bilinearity and the matrix in step 1.2, for and we have , , and . Thus every pair in each increasing root order has positive value.
Segment restrictions in each rank-two plane. For , write as in [F15]. Its extreme positive roots are by step 2.1. By [F8], their reflections are ; [F9] puts every generator of in , while [F10] gives . Thus . By [F2], this subgroup has the two-generator Coxeter presentation with exponent . Its relations reduce every word to one of for ; the inversion sets below show these six elements are distinct. On , [F7], [F11], and [F12] give and . The restrictions for , respectively, are by these actions and [F16]. They are exactly the empty, initial, and final segments in the rank-two criterion [F15]. The sign computation in step 3.1 gives the positive orientation.
Conclusion. Steps 1.2-4.1 and 1.3 verify (i)-(iv) by exact matrix and root calculations. The computation is finite and makes no choice from an infinite family, so AC is not used.
A source–sink move in A3: transporting the Euler and skew forms by an initial letter
Statement
Let be of type , with initial letter , and let , a reduced Coxeter word for the conjugate Coxeter element ; in the generator is final instead of initial, a source-sink move. For the forms of one computes, in the ordered basis , that is, in the fixed basis one has , , and , , . Then:
(i) The conjugation identities of The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (3) hold: and for all taken from the simple basis. For example, using , and : and similarly for the remaining pairs.
(ii) The orientation of the rank-two subsystem changes sign when expressed in its canonical generators: in the relative order is before , in it is before , and correspondingly while ; the transported form is the same form read after applying the reflection to the two canonical roots. This is the sign convention used in The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (4): the forms transport by conjugation while the orientation on the fixed canonical roots reverses. No Axiom of Choice is used.
Facts & Assumptions
Given: the type- Coxeter matrix with , the presented group , the space with its simple basis , the Coxeter form , the canonical reflection representation , the words and , and the forms , .
Coxeter elements, the oriented Euler form, the skew form, and the periodic word (1),(2): a Coxeter word uses each element of once; for a chosen ordered word, and when , when , when , with .
Coxeter words are commutation-connected; the Euler and skew forms depend only on the Coxeter element (1): every Coxeter word is reduced, and every reduced expression of a Coxeter element is again a Coxeter word.
The real Coxeter form, its radical, reflections, and form-preserving maps (2),(3): , , , and for .
The canonical reflection homomorphism, roots, reflections, and the positive cone (1): is a homomorphism with for every .
Coxeter elements, the oriented Euler form, the skew form, and the periodic word (2) combined with The real Coxeter form, its radical, reflections, and form-preserving maps (2),(3): for the word the triangular rule with , and gives the simple-basis entries , , , , , and the diagonal entries , hence , and .
The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (3): if is initial in , then for all one has and .
Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the presentation has the relator for every .
Proof
The word evaluates to using [F7], and it uses each of once, so is a Coxeter word and, by [F2], a reduced Coxeter word for the conjugate Coxeter element ; in it is the final letter. This is the source-sink move.
Compute in the ordered basis from [F1] and the entries of [F3]: , , . Since precedes , which precedes in the word , the triangular rule gives , , , , and the three upper-triangular entries . This is the displayed matrix; subtracting its transpose gives the displayed . In the fixed basis the read-off entries are , , , while , , and .
The reflection acts on the simple basis by [F3] and [F4]: , , and .
Check on the nine simple pairs, using bilinearity, step 1.3, the entries of step 1.2 and the values of [F5]. Pair : . Pair : . Pair : . Pair : . Pair : . Pair : . Pair : . Pair : . Pair : . All nine pairs agree, so by bilinearity the identity holds on all of .
Transport of : since and by [F1], and since is linear and preserves the pairing of arguments' roles, step 2.1 gives for all basis vectors, hence for all vectors by bilinearity. This proves (i) by direct computation, illustrating the general identity [F6].
Clause (ii): from [F5], , and step 1.2 gives . In the noncommuting pair occurs in the order before , so the oriented entry is ; in the same pair occurs in the reversed order before , and the oriented entry is , positive in the reversed order. Moreover step 3.1 with exhibits the transported identity : the new form is the old form read after applying to the two canonical roots, so the forms are conjugate, while the sign on the fixed ordered canonical roots is reversed. This is the sign convention used in the rank-two alignment definition.
Conclusion: steps 1.1-1.3, 2.1, 3.1 and 4.1 verify (i) and (ii) by exact matrix and basis-pair computations. Every witness is a fixed basis vector or a fixed word, so no Choice is used.
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].
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
- A. Bjorner and F. Brenti, Combinatorics of Coxeter Groups, Graduate Texts in Mathematics 231, Springer 2005
- N. Reading, Sortable elements and Cambrian lattices, arXiv:math/0512339v1 (2005); Algebra Universalis 56 (2007) 35-56