LemmaStatement: Literature-sourcedProof: AI-generated

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.

Only finitely many hyperplanes separate two Tits-cone points

PDF p. 8: Lemma 3.5

Statement

Let $(W, S)$ be a Coxeter system, with geometric roots $Φ = Φ^{+} ⊔ Φ^{-}$ in the real vector space with simple-root basis $(α_{i})_{i \in Γ_{0}}$ , and let $Θ$ be its algebraic dual with the contragredient action. Put $\overline{C} = {h \in Θ : h (α_{i}) \geq 0 for every i \in Γ_{0}}$ and $C o n e = ⋃_{w \in W} w \overline{C}$ . For $α \in Φ$ put $H_{α} = {h \in Θ : h (α) = 0}$ and $H = {H_{α} : α \in Φ}$ . Say that $H_{α}$ separates $f, g \in C o n e$ when $f (α)$ and $g (α)$ have opposite strict signs.

For $f, g \in C o n e$ , only finitely many hyperplanes in $H$ separate $f$ and $g$ . The generating set may be infinite; in finite rank these conventions agree with the stated Tits-cone and separation definitions.

Statement references

Coxeter-system, roots, length and weak-order conventions

Reflecting hyperplanes, fundamental chamber and Tits cone

Separation by a hyperplane

Root-sign and inversion-length facts

Facts & Assumptions

[F1]

Each root has exactly one of the two signs, $Φ^{+} = Φ \cap \sum_{i} R_{\geq 0} α_{i}$ and $Φ^{-} = - Φ^{+}$ . For every $w \in W$ , the set ${α \in Φ^{+} : w α \in Φ^{-}}$ has cardinality $ℓ (w)$ and is therefore finite. Root-sign and inversion-length facts

[F2]

Every vector in the geometric representation is a finite linear combination of simple roots. Each root is the image of a simple-root basis vector under an invertible representation map, and $(w h) (v) = h (w^{- 1} v)$ for the contragredient action. Coxeter-system, roots, length and weak-order conventions

[F3]

In finite rank, the nonnegative chamber, its translates, root hyperplanes and opposite-strict-sign separation are the conventions in the cited definitions. Reflecting hyperplanes, fundamental chamber and Tits cone Separation by a hyperplane

Proof

Given: The Coxeter system, root notation and points $f, g \in C o n e$ in the Statement.

Proof technique: direct.

Goal: Show that the set of separating root hyperplanes is finite.

1.1F2algebragiven

Independence of the root representative. Every root $β$ is nonzero, since it is an invertible image of a basis vector by [F2]. A nonzero simple-root coefficient of $β$ gives, by scaling the corresponding coordinate functional, an $h_{0} \in Θ$ with $h_{0} (β) = 1$ . For every $h \in Θ$ , the vector $h - h (β) h_{0}$ belongs to $H_{β}$ ; hence $Θ = R h_{0} \oplus H_{β}$ and $H_{β}$ is a linear hyperplane. If another root $γ$ has $H_{γ} = H_{β}$ , applying evaluation at $γ$ to this vector gives $h (γ) = c h (β)$ for all $h \in Θ$ , where $c = h_{0} (γ)$ . Evaluation at $γ$ is nonzero by the same coordinate argument, so $c \neq 0$ . Consequently $f (γ) g (γ) = c^{2} f (β) g (β)$ , and opposite strict signs are independent of the root representative. This argument works for any rank and uses only coordinate functionals on the given basis.

1.2F1F2given

For any $x \in C o n e$ choose $w \in W$ and $h \in \overline{C}$ with $x = w h$ . If $α \in Φ^{+}$ and $x (α) < 0$ , then $h (w^{- 1} α) < 0$ by [F2]. A positive root is a finite nonnegative linear combination of simple roots, so $h$ evaluates it nonnegatively. By the sign decomposition in [F1], $w^{- 1} α$ must therefore be negative. Hence ${α \in Φ^{+} : x (α) < 0}$ is contained in the finite inversion set ${α \in Φ^{+} : w^{- 1} α \in Φ^{-}}$ .

2.1F1F3step 1.1step 1.2given∎

For each separating hyperplane $H_{β}$ , one of $β$ and $- β$ is positive by [F1], and both define the same hyperplane. For that positive root $α$ , opposite strict signs imply $f (α) < 0$ or $g (α) < 0$ . Thus every separating hyperplane is the image, under $α \mapsto H_{α}$ , of a member of the union of the two finite sets obtained in 1.2 for $x = f$ and $x = g$ . That union and its image are finite, proving the claim. The identification in [F3] gives the finite-rank formulation in the article's geometric conventions.

Depends on

Used by · 1

Finite pair separation yields a finite relative ball

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Normalisers of parabolic subgroups of Artin–Tits groups and Tits cone intersections · PDF p. 8, Lemma 3.5