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 Reflection Arrangements and Spherical Coxeter Complexes — 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
- 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 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
- Fubini and Change of Variables
- Further Trigonometric Identities and Inverse Functions
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- 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
- Improper and Parameter-Dependent Multiple Integrals
- 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
- Mixed Partials, Taylor Formulae, and Extrema
- 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
- Partitions of Unity and Paracompactness
- Permutation Statistics, Inversions and Eulerian Numbers
- 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
- Regular Surfaces and Surface Integrals
- 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 Divergence Theorem and Classical Stokes
- The Fundamental Theorem of Finite Abelian Groups
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- 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
2 · Summary
This draft companion is a dependency leaf. Its exercises and examples use the theory of finite-reflection-arrangements-and-spherical-coxeter-complexes, together with the established prerequisites hilbert-space-geometry-and-riesz-representation for inner-product geometry, further-trigonometric-identities-and-inverses for principal angles, permutation-statistics-inversions-and-eulerian-numbers for finite permutation counts, and the-divergence-theorem-and-classical-stokes for the finite-Jordan integration results used in the sphere-area computation. No other theory page may depend on a supplier homed here.
Three worked computations test the constructions. The Coxeter complex of : the circle triangulated by the ten chambers computes the rank-two complex of : ten chambers, ten vertices, five root lines, the explicit dual vectors with , and the circle triangulated by a decagon. The Coxeter complex of : a triangulation of the sphere and the residue of a proper parabolic counts the complex — triangles, edges, vertices — with the vertex types and their parabolic residues (the hexagon and the four-cycle), the dihedral angles , and the reversal permutation as the longest element with ; each chamber has area and the total sphere area is , proved by a finite-patch calculation and chamber symmetry. Infinite dihedral type: the chamber system is a line, not a sphere; the contractible model is deferred computes the degenerate rank-two case : the chamber system is a line, , there is no opposite chamber, and is infinite with unbounded. The contractible model for infinite (the Davis complex) belongs to the later page spherical-parabolic-cosets-and-the-davis-complex and is not used here.
Each example states all hypotheses and verifies the claimed calculation. A drawing or symbolic calculation alone does not certify a general theorem; the general statements tested here are proved on the theory page finite-reflection-arrangements-and-spherical-coxeter-complexes.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
The Coxeter complex of : the circle triangulated by the ten chambers
Example
Let with and put , so that and (The real Coxeter form, its radical, reflections, and form-preserving maps, Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (3)); let , , the faces , the sphere , the coset face poset and the triangulation be as in The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset and The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere. Then:
(i) is positive definite, , , , and the arrangement consists of the five distinct root lines ().
(ii) The five root lines cut into ten arcs, and these arcs are exactly the spherical chambers (); the complex is a circle triangulated by ten edges and ten vertices, five of type (the cosets ) and five of type (the cosets ), with combinatorial Euler characteristic (the number of vertices minus the number of edges).
(iii) The -dual vectors are and , with and ; hence the two vertices and of the fundamental chamber satisfy , so that every spherical chamber subtends the angle at the centre, and the ten arcs account for the full turn .
(iv) Each vertex of lies in exactly two chambers and each chamber has exactly two vertices; the residue of a vertex of the coset is the Coxeter complex of the rank-one parabolic , namely the two chambers and , and symmetrically for the cosets .
(v) The longest element satisfies , , , and , ; the permutation of The longest element as the opposition of the chamber, and longest elements of finite parabolics (1)(v) interchanges and .
Facts & Assumptions
Given: the two-element set with , the constant , the space with the Coxeter form , the presented group with length function , the canonical reflection homomorphism with root system , the dual action with chamber , faces and Tits cone , the arrangement , the unit sphere , the coset face poset and the triangulation of The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset and The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere.
and ; the reflection formula is for , and in the ordered basis of one has and , so that for , with , and for (The real Coxeter form, its radical, reflections, and form-preserving maps, Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2), (3)(i)-(iv), The canonical reflection homomorphism, roots, reflections, and the positive cone).
is the group presented on by ; is the homomorphism with , , and (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, The canonical reflection homomorphism, roots, reflections, and the positive cone).
with , and , and is a bijection (Root sign coherence and the action of simple reflections on positive roots (1), (2), The inversion formula , the root-reflection dictionary and strong exchange (1)(iv)).
Chambers and faces of the finite chamber system: , distinct closed chambers have disjoint interiors, for the -dual basis , the assignment is a bijection onto the proper faces with and , and realizes as a simplicial complex with one maximal simplex per chamber (The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1)-(4)).
For , , where is the support of a reduced expression, and ; the subsystem is a Coxeter system with , and symmetrically (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1), (2)).
The longest element: for finite there is a unique with , equivalently with , and then , , and there is a permutation of with for every , equivalently (The longest element as the opposition of the chamber, and longest elements of finite parabolics (1)(i), (ii), (iv), (v), The geometric inversion set of an element of a Coxeter group).
The -dual family: there are with and , and they form a basis of (The dual family associated to a Hamel basis , defined by , The dual family of a finite basis is a basis of the dual space, with the same dimension).
is a norm, for , and for ; for -unit vectors we define their principal angle to be (The induced length is a norm, Principal inverse sine and inverse cosine).
For the determinant of a matrix: , , and the determinant of a triangular matrix is the product of its diagonal entries (Rectangular matrix multiplication and the identity matrix , including zero-sized shapes, For same-sized finite square matrices over a commutative ring, , The determinant of a triangular matrix is the product of its diagonal entries).
For a subgroup of a finite group , the coset count is (Lagrange's theorem: for every subgroup of a finite group ).
Verification
The number satisfies : with one has and by the addition formulas, while gives by the shift formula ; hence , that is , and forces , equivalently and .
and is triangular with diagonal entries , so ; with and this gives for every , so no power of equals .
Put . Then , , and therefore for every integer . Substitute into a word in and move every to the right by this identity, cancelling ; the value is or . Since , reduce modulo . Thus has at most ten elements and is finite.
By the positive-definiteness clause of [F1], . The dual vectors are and : with the conditions and read and , that is and ; the computation for is symmetric. Then and , and similarly.
The faces containing a face are exactly the faces with and : if and with then because fixes pointwise and ; conversely makes their intersection equal to . By [F5] that intersection is ; the dual-basis formula of [F5] distinguishes the face types, so . Hence and , giving by [F6], equivalently . Here .
, using and ; consequently and every element of the subgroup generated by and has the form or with .
The root set is : in the basis the matrices of applied to give , , and (using and ), and applying , whose matrix sends and , to those five vectors gives , , , and ; since by step 1.3 every element of is or , the roots () are exactly those ten vectors. The roots are the values and ; the first five are , , , and , and the second five are , , , and , so both families lie in the displayed set and equals it. The five vectors , , , and have pairwise different coordinate pairs in the basis (because : vanishes at but not at ) and lie in , while their negatives lie in ; hence the five are pairwise distinct, and shows that none of the ten is a negative of another of the five, so the displayed set has ten elements. By [F4] each root lies in , so consists exactly of those five vectors: and .
The vertex lies in exactly two chambers, namely and : by step 1.5 with the chambers containing it are the with , and these are distinct. Symmetrically the vertex lies in exactly the chambers and ; every vertex of is of the form or and hence, by the -action, lies in exactly two chambers. Each chamber has exactly the two vertices and , since these are exactly the two one-dimensional faces of by the dual-basis formula of [F5]. The residue of the vertex is therefore the two-point complex , which is the Coxeter complex of the rank-one system , and symmetrically for . This proves (iv).
The ten elements and () are pairwise distinct: the are distinct by and for , the are distinct for the same reason, and is impossible because the left side has determinant while . Hence the image group has at least ten elements, so ; combined with step 1.3 this gives .
By steps 1.3 and 2.2 the group is finite, so the finiteness criterion applies; by clause (1) of Finiteness criterion: W is finite exactly when the Coxeter form is positive definite the form is positive definite. The map is a bijection by [F4], so ; and because , so . The five lines are pairwise distinct: the five positive roots correspond in the coordinates to the directions , , , and ; two of these are proportional only if the corresponding pairs differ by a common nonzero factor, which fails for and against all others (a zero coordinate stays zero) and for the remaining three, as is checked by comparing ratios: versus would force , versus likewise, and versus would force , hence and , contrary to . This proves (i).
Put ; then has matrix , so and ; applied to the five positive roots in the order of step 2.2 this gives , , , and , so and hence .
By [F5] the chamber equals , the cone over the segment , and because are linearly independent; the radial projection of that segment is therefore a continuous injective map of a connected set, so is an arc with endpoints and . Its images under the ten elements of are the ten spherical chambers; by [F5] the closed chambers cover and distinct closed chambers have disjoint interiors, so these ten closed arcs cover the circle and meet only in their endpoints, and the five root lines meet in exactly the ten endpoints; hence the five lines cut into the ten arcs . The triangulation has one edge per chamber and one vertex per coset , ; by [F6] and [F11] these cosets number and , so is a circle with ten edges and ten vertices and Euler characteristic .
Consequently , so the endpoints of the fundamental arc subtend the principal angle . For each the map preserves by [F1] and therefore preserves , so ; hence every spherical chamber subtends the same angle , and the ten arcs account for the full turn .
By [F7] the element with is unique, so ; consequently , , and the permutation of [F7] satisfies ; since and , interchanges and . This proves (v) and completes all clauses.
Remarks
-
The two vertices of the fundamental arc. The arc is cut out by the two walls and through its endpoints and , in agreement with the general vertex description of The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (2).
-
Lengths versus angles. Clause (iii) computes the principal angles subtended by the ten arcs; it does not use, and does not assert, any identification of a path length on with that angle, which belongs to the metric theory of spherical complexes on the in-run page
spherical-simplex-metrics-angular-links-and-cones.
The Coxeter complex of : a triangulation of the sphere and the residue of a proper parabolic
Example
Let with , when and when (type ; thus and ), and let , , the faces , the sphere , the coset face poset and the complex be as in The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset and The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere. Then:
(i) is positive definite and the spherical Coxeter complex is a triangulation of with chambers (triangles), edges and vertices: the vertices are the cosets with , namely the cosets , the cosets and the cosets , where have order and has order ; the combinatorial Euler characteristic (vertices minus edges plus triangles) is .
(ii) The residue (equivalently the link) of a vertex of type with is the Coxeter complex of the rank-two parabolic : exactly chambers contain the vertex and the link is a cycle with edges and vertices. For this is the hexagon of of type , with six chambers and six edges through the vertex, and for the -cycle of of type . The residue of an edge () is two points, and the residue of a chamber is empty.
(iii) The fundamental spherical triangle has dihedral angles , and , that is angle sum , and the chambers are its images under the isometries , , of the sphere, so all chambers are congruent spherical triangles. Each has round surface area , and their total area is , the area of the round unit sphere.
(iv) , , corresponds to the reversal permutation of , and for ; the permutation of The longest element as the opposition of the chamber, and longest elements of finite parabolics (1)(v) is .
Facts & Assumptions
Given: the three-element set with the Coxeter matrix of type , the space with the Coxeter form , the presented group with length function , the canonical reflection homomorphism with root system and reflection set , the dual action with chamber , faces and Tits cone, the arrangement , the unit sphere , the coset face poset with , and the triangulation of The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset and The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere.
The Coxeter data of type : , for , for ; for , for and for ; with the reflection formula for , and every such is -preserving; ; every root has -norm one (The real Coxeter form, its radical, reflections, and form-preserving maps, Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2), The canonical reflection homomorphism, roots, reflections, and the positive cone, Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, Coxeter diagrams: edges, labels, components and finite type, Descent of the reflection representation, unit root norms, and conjugation of reflections (3)).
Type identification: extends to an isomorphism (the library's symmetric group on the letters ), and for every (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4), Inversions, inversion number, the sign , and even and odd permutations).
Parabolic subsystems: for one has with the support, is a Coxeter system whose intrinsic length is the restriction of , and (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1), (2)). Consequently: has order ; the restrictions to and are of type , so by (4) applied with the groups and are isomorphic to of order ; and because , so and has order : the images of these four elements under [F2] are , , and , which are distinct.
The chamber tiling, the dual-basis description of the faces, the face dictionary and the triangulation: ; for the -dual basis one has and ; the assignment is a bijection onto the proper faces with and ; the dihedral angle between and is in the sense of the tangent sector computed in The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (2); and is a finite simplicial complex whose faces have the vertices , with pairwise disjoint relative interiors covering (The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1)-(4)).
Since is finite, there is a unique with , equivalently with ; it satisfies , , is the unique element of maximal length, and there is a permutation of with , equivalently , for every (The longest element as the opposition of the chamber, and longest elements of finite parabolics (1)(i)-(v)).
Finiteness criterion: is finite if and only if is positive definite (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite (1), Positive and negative definiteness, the inertia , rank , and signature of a real symmetric bilinear or quadratic form).
A regular patch is parametrized on a compact Jordan region, and its area is the integral of the Gram density (Regular parametrized surface patches on compact Jordan parameter regions, The first fundamental form, Gram matrix, and area density of a surface patch, Surface area and scalar surface integrals on a regular patch). Injective changes of coordinates with invertible derivative obey compact-Jordan change of variables (Change of variables for an injective map on a compact Jordan set). Bounded sets with content-zero boundary are Jordan measurable; integrals of bounded continuous densities add over finitely many Jordan pieces with content-zero overlaps (A bounded set in is Jordan measurable iff its boundary is null, equivalently of content zero, Additivity of the integral over finitely many Jordan pieces that fill a Jordan set up to content zero).
Sine and cosine have their usual derivatives, Pythagorean identity, signs and endpoint values (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine, Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi). Jordan-Fubini and the second fundamental theorem evaluate rectangular integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable, The second fundamental theorem: if is differentiable on with and is integrable, then ).
For a subgroup of a finite group , (Lagrange's theorem: for every subgroup of a finite group ).
Totally differentiable Euclidean maps obey the chain rule, and a map between open subsets of with invertible derivative has a local inverse (The chain rule for total derivatives: , The Euclidean inverse function theorem).
Closed bounded Euclidean sets are compact, and continuous real functions on nonempty compact sets attain their extrema (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism). The sine and cosine have fundamental period and their stated zero sets (The zero sets of sine and cosine and the least positive common period 2 pi).
A bounded total derivative gives a Lipschitz bound on a convex open Euclidean domain (On a convex open set, a uniform bound implies ). A continuous density on a compact Jordan set is Riemann integrable (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).
Verification
By [F2] and [F3] the group is finite, of order ; hence by [F7] the form is positive definite.
The subgroup orders of [F4] and [F10] give the coset counts for the proper subsets : for the three one-element , and for the values , and for , and .
The faces containing are exactly with and . If , , then because fixes this face pointwise by [F5]; and gives . Conversely, if , their intersection is , so [F5] and the dual-basis formula give . Hence and by [F4], equivalently .
Let be the reversal permutation ; it satisfies because every one of the six pairs is inverted, and for every because an inversion set consists of pairs. Hence attains its maximum at , and by [F6] the longest element is the unique element of maximal length; thus corresponds to the reversal permutation, and and by [F6].
By [F5] the faces of are the cosets with ; a face of type is a spherical simplex on the vertices (). Hence the chambers (type ) number , the edges (type ) number , and the vertices (type , where the simplex is a single point) number by step 1.2; the alternating face count of this triangulation is . Since , [F5] realizes as a triangulation of . This proves the combinatorial part of (i).
Let with and let be a vertex. By step 1.3 the chambers containing are the chambers with , so there are of them; the edges containing are the faces with , (step 1.3 with ), and two such faces coincide exactly when the cosets and coincide, by the dictionary of [F5]. Each chamber through contains exactly the two edges and through ; and each edge through lies, by step 1.3 with , in exactly the two chambers and through . Counting the incidences between the chambers and the edges through by chambers gives twice , and by edges gives twice the number of edges; hence . The chambers through form a connected graph under the relation of sharing an edge, because is generated by its two elements, so the consecutive chambers , share and , share . A connected graph in which every vertex has degree is a cycle; hence the link of is a cycle with edges and vertices, namely with of each. Its chamber edges are indexed by the coset and its vertex edges by the cosets (, ), which is the incidence structure of the Coxeter complex of the parabolic subsystem : for (respectively ) this is the hexagon of with edges, and for the -cycle of . The same count with shows that an edge lies in exactly chambers, so the link of an edge is two points, and the link of a chamber is empty. This proves (ii).
To compute the round area, use orthonormal coordinates for (successively subtract projections from the three basis vectors and divide by their positive norms). Put , and . The coefficient-sum functional satisfies , so on a neighbourhood of ; moreover radial projection is injective on the affine plane , with inverse where . Its derivative on that plane is injective: forces parallel to , whereas and . Thus is a regular patch for . For every , is a regular patch for its chamber, and -invariance gives identical Gram matrices and therefore identical densities . Let ; each chamber has area .
The three vertices of the spherical triangle lie each on a pair of the walls , so by the dihedral-angle clause of [F5] its interior angles are , and , with sum ; every chamber is for a unique , and preserves by [F1], hence is an isometry of carrying onto ; so all chambers are congruent spherical triangles.
Here is the finite chart comparison needed to sum these areas; no independence of an arbitrary surface presentation is assumed. In orthonormal coordinates let and , . This is an injective regular chart, with Gram matrix , so . Cut by the chamber walls and let , . These compact sets are Jordan: away from the latitude-chart seam and poles, great circles have nonzero tangent and their chart preimages are locally smooth arcs; in the radial charts the chamber edges are straight segments, and latitude and longitude boundaries have smooth arc preimages. A finite cover of each compact arc by regular curve pieces suffices. A curve on a neighbourhood of a compact interval has bounded derivative by [F12], and hence a Lipschitz bound there by [F13]; it has content zero in the plane: divide the interval into equal parts and cover each image by a square of side at most times the part length (enlarging by if necessary); the total square area tends to zero. Finite unions and points have the same property, so the boundary criterion in [F8] applies, and the overlaps between different have content zero by [F5]. On a neighbourhood of the transition is an injective coordinate change with invertible derivative: radial projection has the explicit inverse in step 2.3 and the latitude chart has a inverse away from its seam and poles: at each point choose two ambient coordinate components on which its derivative has nonzero determinant and apply [F11]. The remaining sphere coordinate is locally the fixed-sign function , since it is nonzero there; thus the local inverse also applies to , and the inverses agree on overlaps by injectivity of . The chain rule [F11] yields , hence . Change of variables and finite additivity in [F8] now give .
The omitted radial parameter sets approach the preimage of the single longitude seam and the two poles. That compact preimage has content zero: the seam lies on a great circle, whose radial preimage lies on a straight line, and each pole has at most one preimage. For any finite open rectangle cover of that set, compactness places all omitted points in the cover once is sufficiently small: otherwise a compact subset outside the cover would meet arbitrarily narrow seam or pole strips despite its image avoiding the seam and poles. Since is continuous and bounded on , the omitted integral is bounded by its bound times the total area of such a cover, and so tends to zero. There are only patches, hence the left side in step 3.2 tends to . By [F9] the right side is , tending to ; the full latitude patch on itself has area , with its only seam identifications and rank failures on the parameter boundary. Thus the actual finite chamber sum equals the round sphere area, , and . Together with step 3.1 this proves (iii). All covers and coordinate choices are finite; no choice principle is used.
Conjugating the adjacent transposition by the reversal gives , which is the adjacent transposition , that is under the identification of [F2]; hence for . By [F6] the permutation with satisfies , so . This proves (iv).
Remarks
-
The area uses symmetry and finite patch integrals. Steps 2.3, 3.2 and 4.1 prove the needed chart comparison locally and divide the sphere area by the congruent chambers. No spherical-excess theorem or examples-page supplier is used.
-
The residue is an incidence statement. Clause (ii) identifies the residue of a face with the Coxeter complex of the parabolic subsystem through its incidence structure (chambers, edges and their containment). It does not construct an abstract simplicial complex separate from and does not assert a metric identification with a standard simplex.
Infinite dihedral type: the chamber system is a line, not a sphere; the contractible model is deferred
Example
Let with (infinite dihedral type), so that and is positive semidefinite with radical (The real Coxeter form, its radical, reflections, and form-preserving maps, Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order, clause (3)(i)); write a functional as and put . Let , the chambers and the Tits cone be as in The dual action, chambers, faces, and root hyperplanes and The Tits cone, its interior, and the negative-root set of a functional. Then:
(i) The generators act by and , and is -invariant. The fundamental chamber is the closed positive quadrant , and the chambers are the cones over the unit intervals of the affine line ; their relative interiors are pairwise disjoint.
(ii) , so ; the nonzero points of the line lie outside , and .
(iii) There is no with : indeed every nonzero has , hence is disjoint from , while every chamber lies in . Consequently is infinite and the length function is unbounded on , so has no longest element; the spherical conclusion of The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere fails at its finiteness hypothesis.
(iv) The rays of are the nonzero points of the chart : the map is a bijection from onto , and the images of the chambers are the unit intervals . The chamber subdivision is therefore infinite and has no finite subcomplex covering it; in particular the complex is not a finite sphere. The construction of a contractible -complex for infinite (the Davis complex) and its comparison with this chamber system belong to the later page spherical-parabolic-cosets-and-the-davis-complex (order 1768); no result of that page is used or asserted here.
Facts & Assumptions
Given: The Coxeter system with and , the form on , the dual action on with chamber , chambers and Tits cone , and a functional written as with .
is symmetric bilinear with and , and on is positive semidefinite with radical ; the reflection formula is for , so , , , ; the product has matrix with and , so for every (The real Coxeter form, its radical, reflections, and form-preserving maps, Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order, clauses (1)-(3)); and is the canonical reflection homomorphism with root system (The canonical reflection homomorphism, roots, reflections, and the positive cone).
The dual action is , and in the coordinates its generators act by and ; the closed chamber is and the chambers of the chamber system are the sets (The dual action, chambers, faces, and root hyperplanes, The dual action, the faces, and the rank-two chamber tiling, clause (3), The Tits cone, its interior, and the negative-root set of a functional).
The open chambers are pairwise disjoint (Chamber collisions, point stabilizers, and the intersection rule, clause (6)).
if and only if is finite (The interior of the Tits cone, finite parabolic stabilizers, and local finiteness, clause (5)).
Verification
In the coordinates the generators act by the displayed formulas [F2], and both fix : and . Since generates and the dual action is a left action, for every .
The element satisfies and by [F1] its matrix on is with and ; hence for every (for negative use , which holds because ). Therefore in for every , and is infinite.
For with write , so ; then [F2] gives , that is, acts on the line by , and , that is, ; since the action is a left action, acts by and by , so the images of under include every interval and , that is, every unit interval with . Conversely sends a unit interval to and to , both unit intervals, so by induction on length every sends to a unit interval. Since the act linearly and is the cone over , each is the cone over . Hence the chambers are exactly the cones over the unit intervals .
By step 1.2 the group is infinite, so [F4] gives .
By [F1], on gives , and these are pairwise distinct roots for because their -coefficients are distinct; hence is infinite. If were bounded by some natural number , then every element of would be the value of one of the finitely many words in of length at most (using ), so would be finite, contradicting step 1.2. Thus is unbounded on and has no longest element.
Every chamber is the cone over a unit interval of by step 2.1, and every point of such a cone is with and , so is nonnegative on and positive on . Conversely, if then is a real number, hence lies in some unit interval , and then lies in the cone over , which is a chamber; and . Therefore , so the nonzero points of lie outside and .
The relative interior of the chamber which is the cone over is the open cone over , which is the open chamber for the corresponding ; by [F3] these are pairwise disjoint.
If for some , then because every chamber is contained in by step 2.1; but contains for , and since for ( is the open quadrant and ). This contradiction shows that no chamber equals .
The map is well defined on by step 3.1, has values in , is invariant under positive scaling and separates distinct positive rays: if then with positive factor, and conversely positive multiples have the same image; it is surjective onto because gives with by step 3.1. By step 2.1 it carries the chambers onto the unit intervals . The subdivision is infinite because the intervals are pairwise distinct, and no finite union of chambers covers : a finite union of cones over contains no point with and -coordinate , while such points of exist. Hence this chamber system is not a finite sphere; the contractible comparison complex (the Davis complex) belongs to the later page named in the statement and is not used here.
Remarks
-
Consistency with the finite-negativity criterion. For a nonzero with , one has and . By the matrix in [F1], the roots and are positive for every integer , and each family is pairwise distinct. Their values are and . Thus the first family supplies infinitely many negative values when , and the second does so when . Hence has infinitely many negative positive roots, in agreement with The finite-negativity criterion, the reduction step, and convexity of the Tits cone (1), which gives .
-
The negative comparison is the whole of it. This item proves that the finiteness hypothesis in the spherical tiling and triangulation cannot be dropped, and it stops there: it asserts nothing about a contractible complex on which acts, and it declares no dependency on the later page that supplies one.