Alphabeta Math
Pipeline-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.

✓ 4 results · all verified · 2 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Coxeter Euler Forms and Sortable Chamber Cones — Examples

1 · Prerequisites

2 · Summary

This draft companion is a dependency leaf. Its exercises and examples use only the theory of coxeter-euler-forms-and-sortable-chamber-cones and that page’s established prerequisite closure; no other theory page may depend on a supplier homed here.

For c=s1s2s3 in A3 compute the Euler/skew form, all skips of a short sorting word and cone walls. Change c by a source-sink move and check the sign convention. Test a rank-two inversion set violating closure.

Each example states its hypotheses and checks the calculation directly. A counterexample identifies the precise dropped hypothesis; a drawing or symbolic calculation alone does not certify a general theorem.

A2 rank-two inversion-set counterexample

A set of two reflections of A2 that fails both closure and the segment criterion lists every inversion set in A2 and shows that positive-combination closure alone does not recognize inversion sets.

Euler and skew forms in A3

The Euler and skew forms of c = s1s2s3 in A3, and the orientation of its rank-two subsystems computes the Euler and skew forms for c=s1s2s3, checks their signs on the two standard A2 root orders, and recomputes the forms for c′=s1s3s2.

A source–sink move and the sign convention

A source–sink move in A3: transporting the Euler and skew forms by an initial letter conjugates c=s1s2s3 by the initial letter s1, recomputes Ec′ and ωc′ for the reduced Coxeter word c′=s2s3s1, and verifies on all nine basis pairs that the forms transport by ρ(s1) while the sign of the noncommuting pair is prescribed by the order of its letters in the word.

Skips and cone walls for a short sorting word

All skips and the cone walls of the sortable element s1s2 in A3 computes all skips, skip roots, forced and unforced alternatives of the c-sortable element v=s1s2 in A3, identifies the unique cover reflection of v, and verifies the cone inclusion vC⊆Conec(v) predicted by the cone criterion.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

A set of two reflections of A2 that fails both closure and the segment criterion

Statement

Let (W,S) be the Coxeter system of type A2, with S={s,t} and m(s,t)=3. Its reflections and corresponding positive roots in angular order are u1=s,u2=sts,u3=t,βu1=es,βu2=es+et,βu3=et (Plane subsystems, their canonical generators, and the angular order of their roots (2), The real Coxeter form, its radical, reflections, and form-preserving maps (2), The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1)). Put I:={es,et}⊆Φ+.

(i) I is not N(w) for any w∈W; explicitly, N(1)=∅,N(s)={es},N(t)={et},N(st)={et,es+et},N(ts)={es,es+et},N(sts)=Φ+.

(ii) A set is closed under positive rank-two combinations when it contains every root aα+bβ∈Φ+ with a,b>0 and α,β in the set. Then I is not closed: it contains es,et but omits their root es+et. Its complement Φ+∖I={es+et} is closed.

(iii) I is neither an initial nor a final segment of (βu1,βu2,βu3). Thus the rank-two segment criterion of Finite inversion sets are recognized by their rank-two initial or final segments (1)(ii) rejects I.

(iv) By contrast, I′:={es,es+et} is the initial segment (βu1,βu2) and equals N(ts).

(v) The complement Ic:={es+et} is closed under positive rank-two combinations but is not an inversion set. Thus closure of a set alone is insufficient.

Facts & Assumptions

Given: The type-A2 Coxeter system, its canonical real reflection representation, the positive roots and angular order in the Statement, and the inversion-set map N.

[F1]

For a two-dimensional root plane with m=3, the canonical angular list has three positive roots (Plane subsystems, their canonical generators, and the angular order of their roots (2)); the extreme-root rays here are R>0es and R>0et.

[F2]

The reflection subgroup is dihedral of order 6 (Plane subsystems, their canonical generators, and the angular order of their roots (3)); in this rank-two ambient system P=V and the face point is x=0, so that subgroup is W.

[F3]

B(es,es)=B(et,et)=1 and B(es,et)=−12 (The real Coxeter form, its radical, reflections, and form-preserving maps (2)).

[F4]

For a∈{s,t}, ρ(a)v=v−2B(v,ea)ea (The real Coxeter form, its radical, reflections, and form-preserving maps (3)).

[F5]

N(w)={α∈Φ+:ρ(w)α∈Φ−} (The geometric inversion set N(w) of an element of a Coxeter group (1)).

[F6]

A finite positive-root set is an inversion set exactly when its restriction to every noncommutative generalized rank-two subsystem is empty, an initial segment, or a final segment (Finite inversion sets are recognized by their rank-two initial or final segments (1)).

[F7]

For a root α, tρ(w)α=wtαw−1, and the positive roots are in bijection with reflections (The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1)).

Proof

technique · compute the six group actions on the three positive roots, then check closure and the segment condition directly. This is a finite calculation; no Axiom of Choice (AC) is used
1.1F1F3F4F7F8

Finite setup and root order. From [F8], sts=tst; canceling equal adjacent letters and replacing stst by ts and tsts by st reduces every word to one of 1,s,t,st,ts,sts. Hence W is finite and the finite-type suppliers [F1],[F2] apply. Since m(s,t)=3, [F3, F4] give ρ(s)es=−es, ρ(s)et=es+et, ρ(t)es=es+et, and ρ(t)et=−et; by linearity ρ(s)(es+et)=et and ρ(t)(es+et)=es. The orbit definition makes es+et a positive root, and [F1] gives exactly three positive roots in the plane. The extreme rays of V+ are generated by es,et, so their angular order is (es,es+et,et). By [F7], tes+et=stets=sts, while tes=s and tet=t; hence the reflection order is (s,sts,t).

1.2F1

Closure. The roots es,et belong to I, and their positive combination es+et is a root missing from I, so I is not closed. The complement contains only es+et; the positive-root list has no other root on that ray, so every positive combination of two complement members that is a root is again es+et. Hence the complement is closed.

2.1F2F3F4F5

Exhaustive inversion-set calculation. The rank-two presentation gives the six normal forms 1,s,t,st,ts,sts for W by [F2]. Applying step 1.1 with the rightmost generator acting first, the images of (es,es+et,et) under those elements are (es,es+et,et), (−es,et,es+et), (es+et,es,−et), (et,−es,−es−et), (−es−et,−et,es), and (−et,−es−et,−es), respectively. By [F5], their inversion sets are ∅, {es}, {et}, {es+et,et}, {es,es+et}, and Φ+. These six elements exhaust W by [F2], and none of these sets is I.

3.1F1F6

Segment criterion. In the order (es,es+et,et), the initial segments are ∅,{es},{es,es+et},Φ+ and the final segments are ∅,{et},{es+et,et},Φ+. The set I={es,et} is neither. By [F6] it fails the rank-two criterion, agreeing with the exhaustive calculation in step 2.1.

3.2F1F5step 2.1

A valid two-root segment. Step 2.1 gives N(ts)={es,es+et}=I′, the initial segment consisting of the first two roots in the displayed order.

3.3step 1.2step 2.1

The closed non-inversion set. Step 1.2 proves that Ic={es+et} is closed, and the exhaustive list in step 2.1 contains no such singleton inversion set. This proves (v).

4.1F1F2F5F6F7step 1.2step 2.1step 3.1step 3.2step 3.3∎

Conclusion. Steps 1.1-3.3 establish (i)-(v) by finite matrix and set calculations. No witness is selected from an infinite family, so AC is not used.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

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

Statement

Let (W,S) have type A3, with S={s1,s2,s3}, m(s1,s2)=m(s2,s3)=3, and m(s1,s3)=2. Put c=s1s2s3; 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 (es1,es2,es3), the Cartan form K=2B and the forms of Coxeter elements, the oriented Euler form, the skew form, and the periodic word are K=(2−10−12−10−12),Ec=(100−1100−11),ωc=Ec−EcT=(010−1010−10).

(i) Ec+EcT=K, and Ec is lower triangular with diagonal 1, as specified by the ordered word (s1,s2,s3).

(ii) The sign table is ωc(es1,es2)=1>0, ωc(es2,es3)=1>0, and ωc(es1,es3)=0. Thus the commuting pair has zero orientation and each adjacent pair is positive in the order induced by c.

(iii) Put P12:=span⁡{es1,es2}, P23:=span⁡{es2,es3}, W12:=⟨s1,s2⟩, and W23:=⟨s2,s3⟩. 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 P12 and P23. The positive roots in the displayed planes, in angular order from the ray of es1 to that of es2 and from es2 to es3, are (es1,es1+es2,es2) and (es2,es2+es3,es3), respectively. For each ij∈{12,23}, on this root order ωc is positive on all pairs in increasing order. For each subgroup, the restrictions N(w)∩Φ+∩Pij, for w∈Wij, 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′:=s1s3s2, Ec′=(100−11−1001),ωc′=Ec′−Ec′T=(010−10−1010). Thus ωc′(es1,es2)=1 while ωc′(es2,es3)=−1: the orientation of the edge {s2,s3} is reversed and the commuting pair {s1,s3} still has value 0. No Axiom of Choice is used.

Facts & Assumptions

Given: The type-A3 Coxeter matrix, its simple basis, real reflection representation and positive roots, and the two ordered words c and c′.

[F1]
[F2]

Every standard parabolic (WJ,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]
[F6]

For the chosen ordered word, K=2B and Ec(esi,esj)=K(esi,esj) when i>j, 1 when i=j, and 0 when i<j; ωc=Ec−EcT (Coxeter elements, the oriented Euler form, the skew form, and the periodic word (2)).

[F7]

B(es,es)=1 and B(es,et)=−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)es, its associated reflection is tα:=wsw−1; in particular, tes=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∈P⊥ such that B(x,α)≠0 for every root α∉P; for such x the rank-two subgroup W′=Stab⁡W(x) satisfies tα∈W′  ⟺  α∈P (Plane subsystems, their canonical generators, and the angular order of their roots (1)).

[F10]

If r1,r2 are the extreme positive roots in P and a=tr1,b=tr2, 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 es is res(v)=v−2B(v,es)es (The real Coxeter form, its radical, reflections, and form-preserving maps (3)).

[F12]

ρ:W→GL(V) is a homomorphism with ρ(s)=res (The canonical reflection homomorphism, roots, reflections, and the positive cone (1)).

[F13]

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

[F14]

Φ+=Φ∩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)={α∈Φ+:ρ(w)α∈Φ−} (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 S4 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], Kii=2, K12=K21=K23=K32=−1, and K13=K31=0. Applying [F6] in the order (s1,s2,s3) gives exactly the displayed Ec; subtracting its transpose gives the displayed ωc. For x=∑ixiesi, B(x,x)=(x1−x2/2)2+34(x2−23x3)2+23x32, so B is positive definite.

1.3F4F5F6F7

The second Coxeter word. The word c′=s1s3s2 uses each generator once by [F4] and is reduced by [F5]. With its order (s1,s3,s2), [F6]-[F7] give the displayed Ec′ and ωc′ matrices. Their entries yield ωc′(es1,es2)=1, ωc′(es2,es3)=−1, and ωc′(es1,es3)=0, proving (iv).

2.1F1F7F11F12F13F14step 1.2

The two rank-two root lists. Let f1,…,f4 be the standard basis of R4 and let H={x:∑jxj=0}. The vectors αi:=(fi−fi+1)/2 have Gram matrix K/2=B from step 1.2, so esi↦αi extends to an isometry from V to H. Under it, [F11]-[F12] identify ρ(si) with the coordinate transposition (i i+1). Since the adjacent transpositions generate S4 and [F1] identifies W with S4, the root orbit [F13] is exactly {±(fp−fq)/2:p<q}. The positive members are exactly those with p<q, whose simple coordinates are esp+⋯+esq−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 P12 and P23 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 Ec+EcT=K. The entries of ωc give ωc(es1,es2)=1, ωc(es2,es3)=1, and ωc(es1,es3)=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(esi,esi+esi+1)=1, ωc(esi,esi+1)=1, and ωc(esi+esi+1,esi+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=Pi,i+1, write WP=⟨tα:α∈Φ∩P⟩ as in [F15]. Its extreme positive roots are esi,esi+1 by step 2.1. By [F8], their reflections are si,si+1; [F9] puts every generator of WP in W′, while [F10] gives W′=⟨tesi,tesi+1⟩⊆WP. Thus WP=W′=Wi,i+1. By [F2], this subgroup has the two-generator Coxeter presentation with exponent 3. Its relations a2=b2=(ab)3=1 reduce every word to one of 1,a,b,ab,ba,aba for a=si,b=si+1; the inversion sets below show these six elements are distinct. On (x,y,z)=(esi,esi+esi+1,esi+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)∩{x,y,z} for w=1,a,b,ab,ba,aba, respectively, are ∅,{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.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-10-08Open item page →

A source–sink move in A3: transporting the Euler and skew forms by an initial letter

Statement

Let (W,S) be of type A3, c=s1s2s3 with initial letter s=s1, and let c′=scs=s2s3s1, a reduced Coxeter word for the conjugate Coxeter element s1cs1; in c′ the generator s1 is final instead of initial, a source-sink move. For the forms of c′ one computes, in the ordered basis (es2,es3,es1), Ec′=(100−110−101),ωc′=Ec′−Ec′T=(011−100−100), that is, in the fixed basis (es1,es2,es3) one has Ec′(es1,es2)=−1, Ec′(es1,es3)=0, Ec′(es2,es3)=0 and ωc′(es1,es2)=−1, ωc′(es1,es3)=0, ωc′(es2,es3)=1. Then:

(i) The conjugation identities of The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (3) hold: Ec′(ρ(s1)β,ρ(s1)β′)=Ec(β,β′) and ωc′(ρ(s1)β,ρ(s1)β′)=ωc(β,β′) for all β,β′ taken from the simple basis. For example, using ρ(s1)es1=−es1, ρ(s1)es2=es1+es2 and ρ(s1)es3=es3: Ec′(ρ(s1)es1,ρ(s1)es2)=Ec′(−es1,es1+es2)=−Ec′(es1,es1)−Ec′(es1,es2)=−1+1=0=Ec(es1,es2), ωc′(ρ(s1)es1,ρ(s1)es2)=ωc′(−es1,es1+es2)=−ωc′(es1,es1)−ωc′(es1,es2)=0+1=1=ωc(es1,es2), and similarly for the remaining pairs.

(ii) The orientation of the rank-two subsystem W{s1,s2} changes sign when expressed in its canonical generators: in c the relative order is s1 before s2, in c′ it is s2 before s1, and correspondingly ωc(es1,es2)=1 while ωc′(es2,es1)=1; the transported form is the same form read after applying the reflection ρ(s1) to the two canonical roots. This is the sign convention used in The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (4): the forms transport by conjugation while the orientation on the fixed canonical roots reverses. No Axiom of Choice is used.

Facts & Assumptions

Given: the type-A3 Coxeter matrix with S={s1,s2,s3}, the presented group W, the space V=RS with its simple basis (es1,es2,es3), the Coxeter form B, the canonical reflection representation ρ, the words c=s1s2s3 and c′=s1cs1=s2s3s1, and the forms K=2B, Ec,ωc,Ec′,ωc′.

[F1]

Coxeter elements, the oriented Euler form, the skew form, and the periodic word (1),(2): a Coxeter word uses each element of S once; for a chosen ordered word, K=2B and Ec(esi,esj)=K(esi,esj) when i>j, 1 when i=j, 0 when i<j, with ωc=Ec−EcT.

[F2]

Coxeter words are commutation-connected; the Euler and skew forms depend only on the Coxeter element (1): every Coxeter word is reduced, and every reduced expression of a Coxeter element is again a Coxeter word.

[F3]

The real Coxeter form, its radical, reflections, and form-preserving maps (2),(3): B(es,es)=1, B(es1,es2)=B(es2,es3)=−12, B(es1,es3)=0, and ra(v)=v−2B(v,a)B(a,a)a for B(a,a)≠0.

[F4]

The canonical reflection homomorphism, roots, reflections, and the positive cone (1): ρ:W→GL(V) is a homomorphism with ρ(s)=res for every s∈S.

[F5]

Coxeter elements, the oriented Euler form, the skew form, and the periodic word (2) combined with The real Coxeter form, its radical, reflections, and form-preserving maps (2),(3): for the word c=s1s2s3 the triangular rule with K=2B, B(es1,es2)=B(es2,es3)=−12 and B(es1,es3)=0 gives the simple-basis entries Ec(es1,es2)=0, Ec(es1,es3)=0, Ec(es2,es1)=−1, Ec(es2,es3)=0, Ec(es3,es1)=0, Ec(es3,es2)=−1 and the diagonal entries 1, hence ωc(es1,es2)=Ec(es1,es2)−Ec(es2,es1)=1, ωc(es2,es3)=1 and ωc(es1,es3)=0.

[F6]

The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (3): if s is initial in c, then for all β,β′∈V one has Escs(ρ(s)β,ρ(s)β′)=Ec(β,β′) and ωscs(ρ(s)β,ρ(s)β′)=ωc(β,β′).

[F7]

Proof

technique · identify the conjugate word, compute its forms from the triangular rule, then check the conjugation identity on the nine simple-basis pairs directly
1.1F1F2F7given

The word c′=s1cs1 evaluates to s1s1s2s3s1=s2s3s1 using s12=1 [F7], and it uses each of s1,s2,s3 once, so c′ is a Coxeter word and, by [F2], a reduced Coxeter word for the conjugate Coxeter element s1cs1; in it s1 is the final letter. This is the source-sink move.

1.2F1F3algebragiven

Compute Ec′ in the ordered basis (q1,q2,q3)=(es2,es3,es1) from [F1] and the entries K=2B of [F3]: K(es2,es3)=K(es3,es2)=−1, K(es1,es2)=K(es2,es1)=−1, K(es1,es3)=K(es3,es1)=0. Since s2 precedes s3, which precedes s1 in the word c′, the triangular rule gives Ec′(q1,q1)=Ec′(q2,q2)=Ec′(q3,q3)=1, Ec′(q2,q1)=K(es3,es2)=−1, Ec′(q3,q1)=K(es1,es2)=−1, Ec′(q3,q2)=K(es1,es3)=0, and the three upper-triangular entries Ec′(q1,q2)=Ec′(q1,q3)=Ec′(q2,q3)=0. This is the displayed matrix; subtracting its transpose gives the displayed ωc′. In the fixed basis (es1,es2,es3) the read-off entries are Ec′(es1,es2)=Ec′(q3,q1)=−1, Ec′(es1,es3)=Ec′(q3,q2)=0, Ec′(es2,es3)=Ec′(q1,q2)=0, while ωc′(es1,es2)=Ec′(es1,es2)−Ec′(es2,es1)=−1−0=−1, ωc′(es1,es3)=Ec′(es1,es3)−Ec′(es3,es1)=0, and ωc′(es2,es3)=Ec′(es2,es3)−Ec′(es3,es2)=0−(−1)=1.

1.3F3F4algebra

The reflection ρ(s1)=res1 acts on the simple basis by [F3] and [F4]: ρ(s1)es1=−es1, ρ(s1)es2=es2−2B(es2,es1)es1=es1+es2, and ρ(s1)es3=es3−2B(es3,es1)es1=es3.

2.1step 1.2step 1.3F1F3F5algebra

Check Ec′(ρ(s1)eq,ρ(s1)eq′)=Ec(eq,eq′) on the nine simple pairs, using bilinearity, step 1.3, the entries of step 1.2 and the values of [F5]. Pair (q,q′)=(s1,s2): Ec′(−es1,es1+es2)=−Ec′(es1,es1)−Ec′(es1,es2)=−1+1=0=Ec(es1,es2). Pair (s1,s1): Ec′(−es1,−es1)=Ec′(es1,es1)=1=Ec(es1,es1). Pair (s1,s3): Ec′(−es1,es3)=−Ec′(es1,es3)=0=Ec(es1,es3). Pair (s2,s1): Ec′(es1+es2,−es1)=−Ec′(es1,es1)−Ec′(es2,es1)=−1−0=−1=Ec(es2,es1). Pair (s2,s2): Ec′(es1+es2,es1+es2)=Ec′(es1,es1)+Ec′(es1,es2)+Ec′(es2,es1)+Ec′(es2,es2)=1−1+0+1=1=Ec(es2,es2). Pair (s2,s3): Ec′(es1+es2,es3)=Ec′(es1,es3)+Ec′(es2,es3)=0+0=0=Ec(es2,es3). Pair (s3,s1): Ec′(es3,−es1)=−Ec′(es3,es1)=0=Ec(es3,es1). Pair (s3,s2): Ec′(es3,es1+es2)=Ec′(es3,es1)+Ec′(es3,es2)=0−1=−1=Ec(es3,es2). Pair (s3,s3): Ec′(es3,es3)=1=Ec(es3,es3). All nine pairs agree, so by bilinearity the identity holds on all of V.

3.1step 2.1F1F6algebra

Transport of ω: since ωc′=Ec′−Ec′T and ωc=Ec−EcT by [F1], and since ρ(s1) is linear and preserves the pairing of arguments' roles, step 2.1 gives ωc′(ρ(s1)β,ρ(s1)β′)=Ec′(ρ(s1)β,ρ(s1)β′)−Ec′(ρ(s1)β′,ρ(s1)β)=Ec(β,β′)−Ec(β′,β)=ωc(β,β′) for all basis vectors, hence for all vectors by bilinearity. This proves (i) by direct computation, illustrating the general identity [F6].

4.1F5F6step 1.2step 3.1givenalgebra

Clause (ii): from [F5], ωc(es1,es2)=1, and step 1.2 gives ωc′(es2,es1)=1. In c=s1s2s3 the noncommuting pair s1,s2 occurs in the order s1 before s2, so the oriented entry is ωc(es1,es2)=−K(es1,es2)=1; in c′=s2s3s1 the same pair occurs in the reversed order s2 before s1, and the oriented entry is ωc′(es2,es1)=1, positive in the reversed order. Moreover step 3.1 with β=es1,β′=es2 exhibits the transported identity ωc′(ρ(s1)es1,ρ(s1)es2)=ωc(es1,es2): the new form is the old form read after applying ρ(s1) to the two canonical roots, so the forms are conjugate, while the sign on the fixed ordered canonical roots is reversed. This is the sign convention used in the rank-two alignment definition.

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

Conclusion: steps 1.1-1.3, 2.1, 3.1 and 4.1 verify (i) and (ii) by exact matrix and basis-pair computations. Every witness is a fixed basis vector or a fixed word, so no Choice is used.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-10-08Open item page →

All skips and the cone walls of the sortable element s1s2 in A3

Statement

Let (W,S) be of type A3, S={s1,s2,s3}, c=s1s2s3 and v=s1s2. Put Cov(v):={tα:α∈cov⁡(v)} for its cover reflections, with cov⁡(v) the positive-root set of The weak parabolic projection, its adjoints, and the cover-join lemmas (4). Then v is c-sortable, its sorting word is s1s2 at positions 1,2 of the first block of c∞, and its block sequence is the single subset {s1,s2}. (i) The leftmost unselected occurrences are s1 at position 4, s2 at position 5 and s3 at position 3; each skip has i=2, so the associated reflections are ts1=s1s2s1s2s1=s2, ts2=s1s2s1 and ts3=s1s2s3s2s1. The words s1s2s1 and s1s2s3 are reduced while s1s2s2 is not, so the skips of s1 and s3 are unforced and the skip of s2 is forced. (ii) Hence the skip roots are Ccs1(v)=ρ(s1s2)es1=es2,Ccs2(v)=ρ(s1s2)es2=−(es1+es2),Ccs3(v)=ρ(s1s2)es3=es1+es2+es3. These three vectors form a basis of V, Ac(v)={−(es1+es2)} and Bc(v)={es2,es1+es2+es3}. In agreement with Skip roots form a basis, negative skips are cover roots, and the cover decomposition of sortable elements (3), the only element covered by v in the weak order is vs2=s1, so Cov(v)={s1s2s1}, whose positive root is es1+es2. (iii) The cone is Conec(v)={x∈V:B(x,es2)≥0, B(x,es1+es2)≤0, B(x,es1+es2+es3)≥0}, and for every x∈C the translate ρ(v)x satisfies the three inequalities, because of the adjoint identity B(ρ(v)x,β)=B(x,ρ(v)−1β) together with ρ(s1s2)es1=es2, ρ(s1s2)es2=−(es1+es2), ρ(s1s2)es3=es1+es2+es3: explicitly B(ρ(v)x,es2)=B(x,es1)≥0, B(ρ(v)x,es1+es2)=−B(x,es2)≤0 and B(ρ(v)x,es1+es2+es3)=B(x,es3)≥0. Thus vC⊆Conec(v), in agreement with the cone criterion πc(w)=v  ⟺  wC⊆Conec(v) at w=v.

Facts & Assumptions

Given: (W,S) of type A3 with S={s1,s2,s3}, m(s1,s2)=m(s2,s3)=3, m(s1,s3)=2, the Coxeter form B with B(esi,esi)=1, B(es1,es2)=B(es2,es3)=−12, B(es1,es3)=0, the reflection representation ρ, the Coxeter element c=s1s2s3, and v=s1s2.

[F1]

The real Coxeter form, its radical, reflections, and form-preserving maps (2): in the type-A3 normalization B(es,es)=1 for all s∈S, B(es1,es2)=B(es2,es3)=−12 and B(es1,es3)=0.

[F2]

Coxeter elements, the oriented Euler form, the skew form, and the periodic word (1),(3): Ec(esi,esj)=K(esi,esj) for i>j, 1 for i=j and 0 for i<j; c∞ has dividers after each block of n=3 letters and the sorting word is the leftmost reduced subword.

[F3]

c-sortable elements, forced and unforced skips, skip roots, and the chamber cone (1),(2),(3),(4): the definitions of the sorting word, the skips, the associated reflection t=a1⋯air ai⋯a1, forced and unforced skips, the skip roots Ccr(v)=ρ(a1⋯ai)er, the sets Ac(v),Bc(v) and the cone Conec(v).

[F4]

The greedy scan computes the c-sorting word; commutation, conjugation and rank-two alignment (1): the greedy scan selects a position with letter u exactly when u is a left descent of the current remainder and stops at the identity.

[F5]

Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1),(4): the support S(w) of w is independent of the reduced expression, and in type A3 the assignment si↦(i i+1) extends to an isomorphism W→S4; under it the length equals the inversion number of the corresponding permutation.

[F6]

The weak parabolic projection, its adjoints, and the cover-join lemmas (4): the cover roots of w are the roots α∈N(w−1) with tαw=ws and ℓ(ws)=ℓ(w)−1 for some s∈S.

[F7]

Skip roots form a basis, negative skips are cover roots, and the cover decomposition of sortable elements (1),(2),(3): skip roots are ±βt with sign governed by forcedness, the skip set is a basis, and Ac(v)={−βt:t∈Cov(v)}.

[F8]

The cone criterion, monotonicity of the projection, and the greatest sortable element below w (1): for c-sortable v with v≤Rw one has πc(w)=v  ⟺  wC⊆Conec(v).

[F9]

Descent of the reflection representation, unit root norms, and conjugation of reflections (2): ρ(w) is B-preserving, so B(ρ(w)x,β)=B(x,ρ(w)−1β) for all x,β∈V and w∈W.

[F10]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the presentation has the relators s2 for s∈S and (st)m(s,t) for s,t∈S with m(s,t)<∞; in particular s22=1 and (s1s2)3=1.

[F11]

The real Coxeter form, its radical, reflections, and form-preserving maps (3) and The canonical reflection homomorphism, roots, reflections, and the positive cone (1): ra(v)=v−2B(v,a)B(a,a)a for B(a,a)≠0, and ρ(s)=res for every s∈S.

Proof

1.1F2F3F4F5

The element v=s1s2 has ℓ(v)=2 and S(v)={s1,s2} [F5]. The greedy scan of c∞=s1s2s3 s1s2s3⋯ reads the remainders v→s2→1: position 1 has letter s1∈DL(v) and is selected, position 2 has letter s2∈DL(s2) and is selected, and position 3 has letter s3∉DL(1) — the scan stops because the remainder is already 1 after two selections [F4]. Hence the sorting word is s1s2 at positions 1,2 and the block sequence is the single subset {s1,s2}, which is weakly decreasing; so v is c-sortable [F3].

2.1step 1.1F2F3

The selected positions are 1,2, so the leftmost unselected occurrences are s3 at position 3 and s1,s2 at positions 4,5; each follows exactly i=2 selected letters, so all three skips occur in the 3rd position of the sorting word [F3].

3.1step 2.1F3F5F10

The associated reflections are ts1=a1a2s1a2a1=s1s2s1s2s1=s2, ts2=s1s2s2s2s1=s1s2s1 and ts3=s1s2s3s2s1 [F3]; the reductions use (s1s2)3=1 for the first and s22=1 for the second [F10]. The words a1a2s1=s1s2s1 and a1a2s3=s1s2s3 are reduced while a1a2s2=s1s2s2=s1 is not [F5]; hence the skips of s1 and s3 are unforced and the skip of s2 is forced [F3].

4.1step 3.1F1F3F11

The skip roots are Ccs1(v)=ρ(s1s2)es1=es2, Ccs2(v)=ρ(s1s2)es2=−(es1+es2) and Ccs3(v)=ρ(s1s2)es3=es1+es2+es3: the images are computed from [F1] and [F11] as ρ(s2)es1=es1+es2, ρ(s2)es2=−es2, ρ(s2)es3=es2+es3, ρ(s1)es1=−es1, ρ(s1)es2=es1+es2 and ρ(s1)es3=es3, with the sign of the s2-skip negative because that skip is forced [F3].

5.1step 4.1F3algebra

The three vectors es2, −(es1+es2) and es1+es2+es3 form a basis of V: in the basis (es1,es2,es3) they are (0,1,0), (−1,−1,0) and (1,1,1), and the last has a nonzero third coordinate while the first two are independent. By [F3] and step 4.1, Ac(v)={−(es1+es2)} and Bc(v)={es2,es1+es2+es3}.

6.1step 4.1step 5.1F5F6F7F11

Cover reflections: the right descents of v=s1s2 are read off the products vs1=s1s2s1, vs2=s1, vs3=s1s2s3; their lengths are 3, 1 and 3 [F5], so the only cover relation v⋗vs has s=s2 and cover reflection t=vs2v−1=s1s2s1, with positive root −ρ(s1s2)es2=−Ccs2(v)=es1+es2 [F6, F11, step 4.1]. This matches [F7]: the unique negative skip root of v is −(es1+es2) and Cov(v)={s1s2s1}.

7.1step 1.1step 4.1step 5.1F1F3F8F9F11algebra∎

Cone and a chamber check: by [F3] the cone is Conec(v)={x∈V:B(x,es2)≥0, B(x,es1+es2)≤0, B(x,es1+es2+es3)≥0}. For x∈C, i.e. B(x,esi)≥0 for i=1,2,3, the adjoint identity B(ρ(v)x,β)=B(x,ρ(v)−1β) [F9] and the inverse images ρ(v)−1es2=es1, ρ(v)−1(es1+es2)=−es2, ρ(v)−1(es1+es2+es3)=es3 [F11, step 4.1] give B(ρ(v)x,es2)=B(x,es1)≥0, B(ρ(v)x,es1+es2)=−B(x,es2)≤0 and B(ρ(v)x,es1+es2+es3)=B(x,es3)≥0; hence ρ(v)C⊆Conec(v), that is vC⊆Conec(v). This is the instance πc(v)=v of the cone criterion at w=v [F8], consistent with v being c-sortable [step 1.1].

Sources