ExampleConstruction: AI-adaptedVerification: 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.

Ordered roots and the mu-dot-root matrix in A3

Example

Work in the standard realization of $A_{3} = S_{4}$ . Let $E_{1}, \dots, E_{4}$ be the coordinate vectors, put $V_{0} : = {x \in R^{4} : \sum_{i} x_{i} = 0}$ , and use $B (x, y) : = \frac{1}{2} \sum_{i} x_{i} y_{i}$ . Put $σ_{1} : = E_{1} - E_{2}$ , $σ_{2} : = E_{3} - E_{4}$ , $σ_{3} : = E_{2} - E_{3}$ and let $s_{1} = (1 2)$ , $s_{2} = (3 4)$ , $s_{3} = (2 3)$ be their reflections. Thus $J = {s_{1}, s_{2}}$ , $K = {s_{3}}$ , and $c = s_{1} s_{2} s_{3}$ . For $i < j$ , write $(i j)$ for the positive root $E_{i} - E_{j}$ . Multiplication of permutations is right to left. Let $ℓ$ be Coxeter word length and $ℓ_{T}$ reflection length. Then:

(i) Ordered roots. One has $c = (1 2 4 3)$ , $h = 4$ , and $ρ_{1} = (1 2), ρ_{2} = (3 4), ρ_{3} = (1 4), ρ_{4} = (2 4), ρ_{5} = (1 3), ρ_{6} = (2 3) .$ In the simple-root basis these are $σ_{1}, σ_{2}, σ_{1} + σ_{2} + σ_{3}, σ_{2} + σ_{3}, σ_{1} + σ_{3}, σ_{3}$ . Hence $Φ_{+} = {ρ_{1}, \dots, ρ_{6}}$ , $∣ Φ_{+} ∣ = ℓ (w_{0}) = n h / 2 = 6$ , and $ρ_{i + 3} = C_{V} ρ_{i}$ for $i \geq 1$ , where $C_{V} = ρ (c)$ .

(ii) The $μ$ -root matrix. The matrix $(B (μ_{i}, ρ_{j}))_{1 \leq i, j \leq 6}$ is $(\begin{array}{cccccc} 1 & 0 & 1 & 0 & 1 & 0 \\ 0 & 1 & 1 & 1 & 0 & 0 \\ 0 & 0 & 1 & 1 & 1 & 1 \\ - 1 & 0 & 0 & 1 & 0 & 1 \\ 0 & - 1 & 0 & 0 & 1 & 1 \\ - 1 & - 1 & - 1 & 0 & 0 & 1 \end{array}) .$ Its diagonal and upper-triangular entries are nonnegative, its strictly lower-triangular entries are nonpositive, and the first two subdiagonals vanish, as in The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma] (2)(b)-(d).

(iii) The longest word and the second half. The longest element is $w_{0} = c^{2} = (1 4) (2 3)$ and $(s_{1} s_{2} s_{3})^{2}$ is a reduced expression of length $6 = n h / 2$ , with prefix roots $ρ_{1}, \dots, ρ_{6}$ . The prefix roots of $(s_{1} s_{2} s_{3})^{4}$ are $ρ_{1}, \dots, ρ_{12}$ , and $ρ_{7}, \dots, ρ_{12} = - ρ_{2}, - ρ_{1}, - ρ_{3}, - ρ_{5}, - ρ_{4}, - ρ_{6},$ so the second half is $- Φ_{+}$ .

(iv) One factorization-criterion instance. For the pair $(ρ_{1}, ρ_{2})$ , $ℓ_{T} (R (ρ_{1}) R (ρ_{2}) c) = 1 = n - 2 ⟺ B (μ (ρ_{2}), ρ_{1}) = 0.$

No Choice is used.

Facts & Assumptions

Given: The type- $A_{3}$ coordinate model and the bipartite data just specified, together with the conventions of the cited root and reflection items.

[F1]

The Coxeter form and reflection formula are those of The real Coxeter form, its radical, reflections, and form-preserving maps; the canonical representation preserves the form and identifies root reflections with their orthogonal actions by Descent of the reflection representation, unit root norms, and conjugation of reflections. The ordered simple generators $(s_{1}, s_{3}, s_{2})$ are the standard type- $A_{3}$ chain, so the group is $S_{4}$ and Coxeter word length is permutation inversion number by Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4).

[F2]

The dual vectors $β_{i}$ , prefix-root and dual-vector recursions, and $ρ_{i + 3} = C_{V} ρ_{i}$ , $μ_{i + 3} = C_{V} μ_{i}$ are as in The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a (2)-(4). For this irreducible rank-three system with $h = 4$ , The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id (3)-(4) gives $Φ_{+} = {ρ_{1}, \dots, ρ_{6}}$ and the longest-word formula.

[F3]

For each positive root $a$ , $μ (a) = μ_{i}$ when $a = ρ_{i}$ , $B (μ_{i}, ρ_{i}) = 1$ , and the sign and zero-pairing rules in The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma] (1)-(2) apply.

[F4]

Reflection length $ℓ_{T} (w)$ is the minimum number of reflections in $T$ whose product is $w$ ; the empty product represents the identity. Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator (1)

[F5]

For an increasing tuple $a_{1} < \dots < a_{k}$ , the length equality $ℓ_{T} (R (a_{1}) \dots R (a_{k}) c) = n - k$ is equivalent to $B (μ (a_{i}), a_{j}) = 0$ for every $i > j$ . The factorization criterion, linear independence of the faces, and the geometric simplicial structure of X(sigma) (1)

Verification

technique · compute in the simple-root basis, with the standard coordinate action fixing all signs and permutation products

1.1F1

The Gram matrix of $(σ_{1}, σ_{2}, σ_{3})$ is $G = (\begin{array}{ccc} 1 & 0 & - 1 / 2 \\ 0 & 1 & - 1 / 2 \\ - 1 / 2 & - 1 / 2 & 1 \end{array})$ , with determinant $1 / 2 > 0$ ; $B$ is positive definite as it is half the Euclidean form on $V_{0}$ . Thus the map from the abstract simple-root basis to $(σ_{1}, σ_{2}, σ_{3})$ is an isometry. In this basis $C_{V} = (\begin{array}{ccc} 0 & 1 & - 1 \\ 1 & 0 & - 1 \\ 1 & 1 & - 1 \end{array})$ . For any $i < j$ , the reflection with normal $E_{i} - E_{j}$ sends $x$ to $x - (x_{i} - x_{j}) (E_{i} - E_{j})$ and swaps coordinates $i, j$ . Thus the generators act as the stated transpositions, $c = (1 2 4 3)$ , and its order is $4$ .

2.1F1F2step 1.1

The prefix convention gives $ρ_{1} = σ_{1}$ , $ρ_{2} = σ_{2}$ , and $ρ_{3} = R (σ_{1}) R (σ_{2}) σ_{3} = E_{1} - E_{4}$ . Applying $c$ to these roots gives $E_{2} - E_{4}$ , $E_{1} - E_{3}$ , $E_{2} - E_{3}$ , respectively, which are $ρ_{4}, ρ_{5}, ρ_{6}$ . The roots of this coordinate realization are exactly $\pm (E_{i} - E_{j})$ ; the six displayed vectors are exactly the ones with $i < j$ , and their listed simple-root coordinates are nonnegative. This verifies the order, positivity, and full positive-root set in (i), while the cyclic recursion gives $ρ_{i + 3} = C_{V} ρ_{i}$ for all $i \geq 1$ .

3.1F2F3step 2.1

Inverting $G$ gives $G^{- 1} = (\begin{array}{ccc} 3 / 2 & 1 / 2 & 1 \\ 1 / 2 & 3 / 2 & 1 \\ 1 & 1 & 2 \end{array})$ , so $β_{1} = (3 / 2, 1 / 2, 1)$ , $β_{2} = (1 / 2, 3 / 2, 1)$ , and $β_{3} = (1, 1, 2)$ in the simple-root basis. Since $B (β_{2}, σ_{1}) = 0$ and $B (β_{3}, σ_{1}) = B (β_{3}, σ_{2}) = 0$ , the prefix formula gives $μ_{1} = β_{1}$ , $μ_{2} = β_{2}$ , and $μ_{3} = β_{3}$ ; the cyclic recursion gives $μ_{4} = (- 1 / 2, 1 / 2, 1)$ , $μ_{5} = (1 / 2, - 1 / 2, 1)$ , and $μ_{6} = (- 1, - 1, 0)$ . Taking $B (μ_{i}, ρ_{j}) = μ_{i}^{T} G ρ_{j}$ yields exactly the displayed matrix. Reading its entries proves the diagonal, sign, and two-subdiagonal zero assertions.

3.2F1F2step 2.1

Since $c = (1 2 4 3)$ , $c^{2} = (1 4) (2 3)$ is the reverse permutation $(4, 3, 2, 1)$ and has six inversions, the maximum possible in $S_{4}$ . Thus $w_{0} = c^{2}$ and $ℓ (w_{0}) = 6$ . The six-letter word $c^{2} = (s_{1} s_{2} s_{3})^{2}$ is therefore reduced. Applying $C_{V}^{2}$ to $ρ_{1}, \dots, ρ_{6}$ gives $- ρ_{2}, - ρ_{1}, - ρ_{3}, - ρ_{5}, - ρ_{4}, - ρ_{6}$ ; the period-three prefix recursion then gives the twelve prefix roots of $c^{4}$ , with its second half exactly $- Φ_{+}$ .

4.1F4F5step 3.1∎

The matrix in step 3.1 has $B (μ_{2}, ρ_{1}) = 0$ . Also, using $R (ρ_{1}) = (1 2)$ and $R (ρ_{2}) = (3 4)$ , $R (ρ_{1}) R (ρ_{2}) c = (1 2) (3 4) (1 2) (3 4) (2 3) = (2 3)$ , a nonidentity reflection. Hence its reflection length is $1 = n - 2$ , so both sides of the stated equivalence hold for this pair.

Depends on

Used by

In A3 the moved spaces meet in a line, while the root complexes have no common nonempty face Example

Dependency tree · two levels

78 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

Thomas Brady and Colum Watt, Lattices in finite real reflection groups (arXiv:math/0501502, 29-page PDF) (standard reference, not scraped)
Robert Steinberg, Finite reflection groups, Transactions of the American Mathematical Society 91 (1959) 493-504 (AMS free digital archive, 12-page PDF) (standard reference, not scraped)
Bill Casselman, Essays on Coxeter groups: Coxeter elements in finite Coxeter groups (author-hosted PDF, 12 pages) (standard reference, not scraped)
Sergey Fomin and Nathan Reading, Root systems and generalized associahedra, IAS/Park City Mathematics Series lecture notes (arXiv:math/0505518) (standard reference, not scraped)