ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

A vector with mixed signs is not a root, while every root has a sign

Example

Let $S = {s, t}$ with $m (s, t) \geq 3$ , $V = R^{S}$ , $B$ the Coxeter form and $Φ$ the root system of the canonical reflection representation (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone). Then:

(i) the vector $v : = e_{s} - e_{t}$ has coefficient $- 1$ at $e_{t}$ , so $v \notin V_{+} \cup (- V_{+})$ : it has mixed signs;

(ii) consequently $v \notin Φ$ , although it is nonzero and $B$ -non-isotropic, because by Root sign coherence and the action of simple reflections on positive roots (2) every root lies in $V_{+} ∖ {0}$ or in $- V_{+} ∖ {0}$ ; explicitly $B (v, v) = 2 + 2 c (s, t) > 0$ while every root has $B$ -norm $1$ (Descent of the reflection representation, unit root norms, and conjugation of reflections (3)), so $v$ fails both the sign test and the norm test;

(iii) for $m (s, t) = 3$ one has $B (v, v) = 3$ and the comparison case $e_{s} + e_{t}$ has $B (e_{s} + e_{t}, e_{s} + e_{t}) = 1$ and lies in $Φ_{+}$ ; for $m (s, t) = \infty$ one has $B (v, v) = 4$ and $v$ still fails to be a root.

Facts & Assumptions

Given: a two-element set $S = {s, t}$ with $m : = m (s, t) \geq 3$ , the space $V = R^{S}$ with basis $(e_{s}, e_{t})$ , the Coxeter form $B$ , the canonical reflection homomorphism $ρ$ , the root system $Φ = Φ_{+} ⊔ Φ_{-}$ and the positive cone $V_{+}$ .

[F1]

$B (e_{s}, e_{s}) = B (e_{t}, e_{t}) = 1$ and $B (e_{s}, e_{t}) = - c$ with $c : = c (s, t)$ equal to $\cos (π / m)$ when $m < \infty$ and to $1$ when $m = \infty$ ; the reflection with normal $e_{t}$ is $r_{t} (u) = u - 2 B (u, e_{t}) e_{t}$ , so $ρ (t) e_{s} = r_{t} e_{s} = e_{s} + 2 c e_{t}$ ; and $V_{+} = {λ e_{s} + μ e_{t} : λ \geq 0, μ \geq 0}$ with $- V_{+} = {u : - u \in V_{+}}$ (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone).

[F2]

Every root lies in $V_{+} ∖ {0}$ or in $- V_{+} ∖ {0}$ , and not in both; every root $α$ satisfies $B (α, α) = 1$ ; $Φ_{+} = Φ \cap V_{+}$ (Root sign coherence and the action of simple reflections on positive roots, Descent of the reflection representation, unit root norms, and conjugation of reflections).

[F3]

For every $x \in W$ and every generator $s$ one has $x C^{\circ} \subseteq B_{s}$ or $x C^{\circ} \subseteq s B_{s}$ , and $x C^{\circ} \subseteq s B_{s}$ if and only if $ℓ (s x) < ℓ (x)$ ; moreover $ρ (y) e_{s} \in Φ_{+} ⟺ y^{- 1} C^{\circ} \subseteq B_{s}$ for the root $ρ (y) e_{s}$ (The rank-two half-space alternative and the chamber-length induction $(P_{n})$ , $(Q_{n})$ , Root sign coherence and the action of simple reflections on positive roots).

[F4]

The simple generators are distinct in $W$ , so $s \neq t$ , and $ℓ (t) = 1$ ; moreover $ℓ (x) = 0$ implies $x = 1$ (Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action, Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F5]

The addition formulas $\sin (x + y) = \sin x \cos y + \cos x \sin y$ , $\cos (x + y) = \cos x \cos y - \sin x \sin y$ hold for all real $x, y$ ; $\sin (- x) = - \sin x$ , $\cos (- x) = \cos x$ and $\sin^{2} x + \cos^{2} x = 1$ ; $\cos (π / 2) = 0$ and $\cos π = - 1$ ; cosine is strictly decreasing on $[0, π]$ ; and $π > 0$ (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine, Quarter-turn values and shifts by pi/2 and pi, Signs, monotonicity intervals, and ranges of sine and cosine, Pi as twice the smallest positive zero of cosine).

[F6]

Every $x \in V = R^{{s, t}}$ equals $x (s) e_{s} + x (t) e_{t}$ ; evaluating at $s$ and $t$ shows that these coordinates are unique (Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (1)).

Verification

technique · direct

1.1F1F5algebra

Set-up. By [F1] the vector $v = e_{s} - e_{t}$ has coordinates $v (s) = 1$ and $v (t) = - 1$ in the basis $(e_{s}, e_{t})$ , and $B (v, v) = B (e_{s}, e_{s}) - 2 B (e_{s}, e_{t}) + B (e_{t}, e_{t}) = 2 + 2 c$ . The constant $c$ is positive: $c = 1 > 0$ for $m = \infty$ , while for finite $m \geq 3$ one has $0 < π / m \leq π / 3 < π / 2$ and cosine is strictly decreasing on $[0, π]$ with $\cos (π / 2) = 0$ by [F5], so $c = \cos (π / m) > \cos (π / 2) = 0$ . Hence $B (v, v) > 2 > 0$ , so $v \neq 0$ and $v$ is $B$ -non-isotropic.

1.2F1F6algebra

The vector has mixed signs. By [F6] the coordinates of a vector in the basis $(e_{s}, e_{t})$ are unique, so $u \in V_{+}$ exactly when both coordinates of $u$ are $\geq 0$ and $u \in - V_{+}$ exactly when both coordinates are $\leq 0$ . Since $v$ has the coordinates $1$ and $- 1$ , it lies in neither cone: $v \notin V_{+} \cup (- V_{+})$ . This is (i).

2.1F1F5step 1.1algebra

The value $c = \cos (π / 3)$ . For $x$ with $\cos x = : q$ and $\sin x = : r$ , the addition formulas and $\sin^{2} x + \cos^{2} x = 1$ of [F5] give $\cos (2 x) = q^{2} - r^{2} = 2 q^{2} - 1$ and $\sin (2 x) = 2 q r$ , hence $\cos (3 x) = \cos (2 x) \cos x - \sin (2 x) \sin x = (2 q^{2} - 1) q - 2 q r^{2} = 2 q^{3} - q - 2 q (1 - q^{2}) = 4 q^{3} - 3 q$ . Applied to $x = π / 3$ and combined with $\cos π = - 1$ this gives $4 c^{3} - 3 c + 1 = 0$ , that is $(c + 1) (2 c - 1)^{2} = 0$ . Since $c > 0$ by 1.1, the factor $c + 1$ does not vanish, so $(2 c - 1)^{2} = 0$ and $c = 1 / 2$ . Consequently $2 c = 1$ , $B (v, v) = 2 + 1 = 3$ , and $ρ (t) e_{s} = e_{s} + 2 c e_{t} = e_{s} + e_{t}$ ; moreover $B (e_{s} + e_{t}, e_{s} + e_{t}) = 1 + 1 - 2 c = 2 - 1 = 1$ .

2.2F2step 1.1step 1.2

$v$ is not a root. By [F2] every root lies in $V_{+} ∖ {0}$ or in $- V_{+} ∖ {0}$ , and every root has $B$ -norm $1$ . By 1.2 the vector $v$ lies in neither cone, so it is not a root; independently, by 1.1 its $B$ -norm is $2 + 2 c > 2 \neq 1$ , so it also fails the norm test for roots. This is (ii).

3.1F3F4step 2.1

The comparison vector $e_{s} + e_{t}$ is positive. By [F3] applied to $x = t$ either $t C^{\circ} \subseteq B_{s}$ or $t C^{\circ} \subseteq s B_{s}$ . In the second case $ℓ (s t) < ℓ (t) = 1$ by [F3], so $ℓ (s t) = 0$ and hence $s t = 1$ by [F4], which gives $s = t^{- 1} = t$ and contradicts $s \neq t$ ; therefore $t C^{\circ} \subseteq B_{s}$ , and the equivalence of [F3] with $y = t$ gives $ρ (t) e_{s} \in Φ_{+}$ . By 2.1, $ρ (t) e_{s} = e_{s} + e_{t}$ when $m = 3$ , so $e_{s} + e_{t} \in Φ_{+}$ with $B (e_{s} + e_{t}, e_{s} + e_{t}) = 1$ .

4.1step 2.1step 2.2step 3.1F1∎

The cases $m = 3$ and $m = \infty$ . If $m = 3$ then $c = 1 / 2$ by 2.1, so $B (v, v) = 3$ , and $e_{s} + e_{t} = ρ (t) e_{s}$ is a positive root of $B$ -norm $1$ by 3.1. If $m = \infty$ then $c = 1$ by [F1], so $B (v, v) = 4$ , and $v \notin Φ$ by 2.2. With (i) from 1.2 and (ii) from 2.2, all three clauses are verified: the sign theorem applies to the $W$ -orbit of the simple roots, not to arbitrary vectors of $V$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

83 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

Michael W. Davis, The Geometry and Topology of Coxeter Groups (Princeton University Press, 2008; author's complete institutional PDF) (standard reference, not scraped)
Anders Bjorner and Francesco Brenti, Combinatorics of Coxeter Groups (Graduate Texts in Mathematics 231, Springer 2005; author-hosted full PDF) (standard reference, not scraped)