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

The Euler and skew forms of c = s1s2s3 in A3, and the orientation of its rank-two subsystems

Statement

Let $(W, S)$ have type $A_{3}$ , with $S = {s_{1}, s_{2}, s_{3}}$ , $m (s_{1}, s_{2}) = m (s_{2}, s_{3}) = 3$ , and $m (s_{1}, s_{3}) = 2$ . Put $c = s_{1} s_{2} s_{3}$ ; 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 $(e_{s_{1}}, e_{s_{2}}, e_{s_{3}})$ , the Cartan form $K = 2 B$ and the forms of Coxeter elements, the oriented Euler form, the skew form, and the periodic word are $K = (\begin{array}{ccc} 2 & - 1 & 0 \\ - 1 & 2 & - 1 \\ 0 & - 1 & 2 \end{array}), E_{c} = (\begin{array}{ccc} 1 & 0 & 0 \\ - 1 & 1 & 0 \\ 0 & - 1 & 1 \end{array}), ω_{c} = E_{c} - E_{c}^{T} = (\begin{array}{ccc} 0 & 1 & 0 \\ - 1 & 0 & 1 \\ 0 & - 1 & 0 \end{array}) .$

(i) $E_{c} + E_{c}^{T} = K$ , and $E_{c}$ is lower triangular with diagonal $1$ , as specified by the ordered word $(s_{1}, s_{2}, s_{3})$ .

(ii) The sign table is $ω_{c} (e_{s_{1}}, e_{s_{2}}) = 1 > 0$ , $ω_{c} (e_{s_{2}}, e_{s_{3}}) = 1 > 0$ , and $ω_{c} (e_{s_{1}}, e_{s_{3}}) = 0$ . Thus the commuting pair has zero orientation and each adjacent pair is positive in the order induced by $c$ .

(iii) Put $P_{12} : = span {e_{s_{1}}, e_{s_{2}}}$ , $P_{23} : = span {e_{s_{2}}, e_{s_{3}}}$ , $W_{12} : = ⟨ s_{1}, s_{2} ⟩$ , and $W_{23} : = ⟨ s_{2}, s_{3} ⟩$ . By The inversion formula $∣ N (w) ∣ = ℓ (w)$ , 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 $P_{12}$ and $P_{23}$ . The positive roots in the displayed planes, in angular order from the ray of $e_{s_{1}}$ to that of $e_{s_{2}}$ and from $e_{s_{2}}$ to $e_{s_{3}}$ , are $(e_{s_{1}}, e_{s_{1}} + e_{s_{2}}, e_{s_{2}})$ and $(e_{s_{2}}, e_{s_{2}} + e_{s_{3}}, e_{s_{3}})$ , respectively. For each $i j \in {12, 23}$ , on this root order $ω_{c}$ is positive on all pairs in increasing order. For each subgroup, the restrictions $N (w) \cap Φ_{+} \cap P_{i j}$ , for $w \in W_{i j}$ , 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 $c^{'} : = s_{1} s_{3} s_{2}$ , $E_{c^{'}} = (\begin{array}{ccc} 1 & 0 & 0 \\ - 1 & 1 & - 1 \\ 0 & 0 & 1 \end{array}), ω_{c^{'}} = E_{c^{'}} - E_{c^{'}}^{T} = (\begin{array}{ccc} 0 & 1 & 0 \\ - 1 & 0 & - 1 \\ 0 & 1 & 0 \end{array}) .$ Thus $ω_{c^{'}} (e_{s_{1}}, e_{s_{2}}) = 1$ while $ω_{c^{'}} (e_{s_{2}}, e_{s_{3}}) = - 1$ : the orientation of the edge ${s_{2}, s_{3}}$ is reversed and the commuting pair ${s_{1}, s_{3}}$ still has value $0$ . No Axiom of Choice is used.

Facts & Assumptions

Given: The type- $A_{3}$ Coxeter matrix, its simple basis, real reflection representation and positive roots, and the two ordered words $c$ and $c^{'}$ .

[F1]

For the type- $A_{3}$ matrix, the canonical map to $S_{4}$ is an isomorphism (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4)).

[F2]

Every standard parabolic $(W_{J}, J)$ is a Coxeter system with the restricted matrix (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2)).

[F3]

Finite type (spherical type) means exactly that $W$ is finite (Coxeter diagrams: edges, labels, components and finite type (4)).

[F4]

A Coxeter word uses each element of $S$ once (Coxeter elements, the oriented Euler form, the skew form, and the periodic word (1)).

[F5]

Every Coxeter word is reduced (Coxeter words are commutation-connected; the Euler and skew forms depend only on the Coxeter element (1)).

[F6]

For the chosen ordered word, $K = 2 B$ and $E_{c} (e_{s_{i}}, e_{s_{j}}) = K (e_{s_{i}}, e_{s_{j}})$ when $i > j$ , $1$ when $i = j$ , and $0$ when $i < j$ ; $ω_{c} = E_{c} - E_{c}^{T}$ (Coxeter elements, the oriented Euler form, the skew form, and the periodic word (2)).

[F7]

$B (e_{s}, e_{s}) = 1$ and $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ for finite $m (s, t)$ (The real Coxeter form, its radical, reflections, and form-preserving maps (2)).

[F8]

For a root $α = ρ (w) e_{s}$ , its associated reflection is $t_{α} : = w s w^{- 1}$ ; in particular, $t_{e_{s}} = s$ (The inversion formula $∣ N (w) ∣ = ℓ (w)$ , the root-reflection dictionary and strong exchange (1)).

[F9]

For every root-spanned plane $P$ , there is an $x \in P^{⊥}$ such that $B (x, α) \neq 0$ for every root $α \notin P$ ; for such $x$ the rank-two subgroup $W^{'} = {Stab}_{W} (x)$ satisfies $t_{α} \in W^{'} ⟺ α \in P$ (Plane subsystems, their canonical generators, and the angular order of their roots (1)).

[F10]

If $r_{1}, r_{2}$ are the extreme positive roots in $P$ and $a = t_{r_{1}}, b = t_{r_{2}}$ , then $W^{'} = ⟨ a, b ⟩$ is dihedral (Plane subsystems, their canonical generators, and the angular order of their roots (2),(3)).

[F11]

The reflection with normal $e_{s}$ is $r_{e_{s}} (v) = v - 2 B (v, e_{s}) e_{s}$ (The real Coxeter form, its radical, reflections, and form-preserving maps (3)).

[F12]

$ρ : W \to G L (V)$ is a homomorphism with $ρ (s) = r_{e_{s}}$ (The canonical reflection homomorphism, roots, reflections, and the positive cone (1)).

[F13]

$Φ = {ρ (w) e_{s} : w \in W, s \in S}$ (The canonical reflection homomorphism, roots, reflections, and the positive cone (2)).

[F14]

$Φ_{+} = Φ \cap V_{+}$ , where $V_{+}$ 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)).

[F15]

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)).

[F16]

$N (w) = {α \in Φ_{+} : ρ (w) α \in Φ_{-}}$ (The geometric inversion set $N (w)$ of an element of a Coxeter group (1)).

Proof

technique · compute the Coxeter form entries, apply the triangular Euler-form definition to each word, and evaluate $\omega$ on the two root lists using bilinearity

1.1F1F3F4F5

Finite-type setup. By [F1], $W$ is isomorphic to $S_{4}$ and hence finite; by [F3] it is of finite type. Each displayed word uses every simple generator once by [F4], so [F5] says that $c$ and $c^{'}$ are reduced Coxeter words, as required to define their Euler forms.

1.2F6F7

Cartan and Euler matrices. From [F7], $K_{i i} = 2$ , $K_{12} = K_{21} = K_{23} = K_{32} = - 1$ , and $K_{13} = K_{31} = 0$ . Applying [F6] in the order $(s_{1}, s_{2}, s_{3})$ gives exactly the displayed $E_{c}$ ; subtracting its transpose gives the displayed $ω_{c}$ . For $x = \sum_{i} x_{i} e_{s_{i}}$ , $B (x, x) = (x_{1} - x_{2} / 2)^{2} + \frac{3}{4} (x_{2} - \frac{2}{3} x_{3})^{2} + \frac{2}{3} x_{3}^{2}$ , so $B$ is positive definite.

1.3F4F5F6F7

The second Coxeter word. The word $c^{'} = s_{1} s_{3} s_{2}$ uses each generator once by [F4] and is reduced by [F5]. With its order $(s_{1}, s_{3}, s_{2})$ , [F6]-[F7] give the displayed $E_{c^{'}}$ and $ω_{c^{'}}$ matrices. Their entries yield $ω_{c^{'}} (e_{s_{1}}, e_{s_{2}}) = 1$ , $ω_{c^{'}} (e_{s_{2}}, e_{s_{3}}) = - 1$ , and $ω_{c^{'}} (e_{s_{1}}, e_{s_{3}}) = 0$ , proving (iv).

2.1F1F7F11F12F13F14step 1.2

The two rank-two root lists. Let $f_{1}, \dots, f_{4}$ be the standard basis of $R^{4}$ and let $H = {x : \sum_{j} x_{j} = 0}$ . The vectors $α_{i} : = (f_{i} - f_{i + 1}) / \sqrt{2}$ have Gram matrix $K / 2 = B$ from step 1.2, so $e_{s_{i}} \mapsto α_{i}$ extends to an isometry from $V$ to $H$ . Under it, [F11]-[F12] identify $ρ (s_{i})$ with the coordinate transposition $(i i + 1)$ . Since the adjacent transpositions generate $S_{4}$ and [F1] identifies $W$ with $S_{4}$ , the root orbit [F13] is exactly ${\pm (f_{p} - f_{q}) / \sqrt{2} : p < q}$ . The positive members are exactly those with $p < q$ , whose simple coordinates are $e_{s_{p}} + \dots + e_{s_{q - 1}}$ , by [F14]. In each rank-two plane the three positive roots have coefficient pairs $(1, 0), (1, 1), (0, 1)$ 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 $P_{12}$ and $P_{23}$ are exactly the three displayed in (iii), in the stated angular orders.

2.2F6step 1.2

Symmetrization and simple-root signs. Adding the displayed matrices yields $E_{c} + E_{c}^{T} = K$ . The entries of $ω_{c}$ give $ω_{c} (e_{s_{1}}, e_{s_{2}}) = 1$ , $ω_{c} (e_{s_{2}}, e_{s_{3}}) = 1$ , and $ω_{c} (e_{s_{1}}, e_{s_{3}}) = 0$ .

3.1F6step 1.2step 2.1

All rank-two signs. By bilinearity and the matrix in step 1.2, for $i = 1$ and $i = 2$ we have $ω_{c} (e_{s_{i}}, e_{s_{i}} + e_{s_{i + 1}}) = 1$ , $ω_{c} (e_{s_{i}}, e_{s_{i + 1}}) = 1$ , and $ω_{c} (e_{s_{i}} + e_{s_{i + 1}}, e_{s_{i + 1}}) = 1$ . Thus every pair in each increasing root order has positive value.

4.1F2F3F7F8F9F10F11F12F15F16step 1.1step 1.2step 2.1step 3.1

Segment restrictions in each rank-two plane. For $P = P_{i, i + 1}$ , write $W_{P} = ⟨ t_{α} : α \in Φ \cap P ⟩$ as in [F15]. Its extreme positive roots are $e_{s_{i}}, e_{s_{i + 1}}$ by step 2.1. By [F8], their reflections are $s_{i}, s_{i + 1}$ ; [F9] puts every generator of $W_{P}$ in $W^{'}$ , while [F10] gives $W^{'} = ⟨ t_{e_{s_{i}}}, t_{e_{s_{i + 1}}} ⟩ \subseteq W_{P}$ . Thus $W_{P} = W^{'} = W_{i, i + 1}$ . By [F2], this subgroup has the two-generator Coxeter presentation with exponent $3$ . Its relations $a^{2} = b^{2} = (a b)^{3} = 1$ reduce every word to one of $1, a, b, a b, b a, a b a$ for $a = s_{i}, b = s_{i + 1}$ ; the inversion sets below show these six elements are distinct. On $(x, y, z) = (e_{s_{i}}, e_{s_{i}} + e_{s_{i + 1}}, e_{s_{i + 1}})$ , [F7], [F11], and [F12] give $a (x, y, z) = (- x, z, y)$ and $b (x, y, z) = (y, x, - z)$ . The restrictions $N (w) \cap {x, y, z}$ for $w = 1, a, b, a b, b a, a b a$ , respectively, are $\emptyset, {x}, {z}, {y, z}, {x, y}, {x, y, z}$ 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.

5.1F1step 1.1step 1.2step 1.3step 2.1step 2.2step 3.1step 4.1∎

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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

N. Reading and D. E. Speyer, Sortable elements in infinite Coxeter groups, arXiv:0803.2722v3 (2010); Trans. Amer. Math. Soc. 363 (2011) 699-761 (standard reference, not scraped)