Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass
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 rank-two affine B2 Hecke algebra with unequal parameters

Example

Let E=R2 with the dot product and standard vectors e1,e2. Set

Y=Z(e1−e2)+Z(2e2)={(a,b)∈Z2:a+b is even},X=Ze1+Z12(e1+e2).

The displayed bases of X and Y are dual under the dot product. Let

Φ={±e1,±e2,±(e1+e2),±(e1−e2)},

with coroot α∨=2α for the short roots α=±ei and α∨=α for the long roots α=±e1±e2. Choose Δ={α1=e1−e2,α2=e2}. The affine alcove is

A0={(x1,x2):0<x2<x1, x1+x2<1}.

Its simple reflections are s1(x1,x2)=(x2,x1), s2(x1,x2)=(x1,−x2), and s0(x1,x2)=(1−x2,1−x1). The affine Iwahori–Matsumoto parameters are qs0=qs1=2 on the long-root walls and qs2=3 on the short-root wall.

Facts & Assumptions

Given: The lattice pair X,Y, root and coroot sets, simple roots, and affine alcove stated above.

[F1]

A reduced root datum consists of finite-rank free lattices in perfect integral duality, a finite root set and coroot set in bijection, and Weyl reflections preserving both sets (Abstract root data and their Weyl groups).

[F2]

The Iwahori–Matsumoto algebra uses (Ts−qs)(Ts+1)=0 and the affine Coxeter braid relations; Ns=qs−1/2Ts satisfies (Ns−qs1/2)(Ns+qs−1/2)=0 (The Iwahori–Matsumoto affine Hecke algebra of a based root datum).

[F3]

For a reduced crystallographic root system, affine reflections in the integer root hyperplanes generate the affine Coxeter group, whose simple reflections are those of the fundamental alcove; the product order of two simple wall reflections is determined by the angle between their walls (Affine root hyperplanes, coroot translations, alcoves, and the affine reflection group, Alcove transitivity, the affine Coxeter presentation, and the length function).

[F4]

In the generic Coxeter Hecke presentation, parameters are allowed exactly when they are constant on the odd-edge connected components of the simple-generator graph; simple generators are conjugate exactly within those components (Universal parameters, the generic Coxeter Hecke algebra and generator conjugacy).

[L1]

The elements TwUω form a basis of the extended Iwahori–Matsumoto algebra (The extended Iwahori–Matsumoto basis).

Verification

Given: The proposed B2 root datum and affine Hecke parameters.

1.1F1givenalgebra

The vectors e1 and 12(e1+e2) form a basis of X, while e1−e2 and 2e2 form a basis of Y: an integer pair (a,b) has even coordinate sum exactly when (a,b)=a(e1−e2)+a+b2(2e2). The dot-product matrix between these two bases is the identity, so the pairing is perfect and integral. The roots lie in X, the coroots lie in Y, and direct pairings on α1,α2 give the Cartan matrix (2−2−12). The positive roots are α1,α2,α1+α2=e1,α1+2α2=e1+e2, so Δ is a base and the root set is reduced. The displayed root set is the union of the signed-permutation orbits of α1 and α2. The prescribed coroot map is equivariant under signed permutations: it doubles each short root and fixes each long-root vector, and signed permutations preserve root length. Thus the simple-root checks give ⟨α,α∨⟩=2 for every listed root, and the generated reflections preserve both root sets. The signed-permutation group generated by s1,s2 is finite. Therefore [F1] applies and these data are a reduced based B2 root datum.

1.2F3givenalgebra

The simple walls of A0 are x1=x2, x2=0, and x1+x2=1. In its interior, 0<x2<1, 0<x1−x2<1, and 0<x1+x2<1; the remaining positive-root function satisfies 0<x1<1 because x2>0 and x1+x2<1. Thus no other integer root wall cuts it. Their reflections are respectively the displayed s1,s2,s0. The product s1s2 is (x1,x2)↦(−x2,x1), a quarter-turn of order 4. The product s2s0 is (x1,x2)↦(1−x2,x1−1); it fixes (1,0) and its linear part about that point is the same quarter-turn, so it has order 4. The product s0s1 is (x1,x2)↦(1−x1,1−x2), a half-turn of order 2. Hence the affine Coxeter labels are m(s1,s2)=m(s2,s0)=4 and m(s1,s0)=2.

2.1F2F4step 1.2algebra

The affine roots defining s0 and s1 are long and the one defining s2 is short. The displayed basis of Y is α1∨,α2∨, so Y=Q∨ and Ω=1 by [F2]. Thus conjugacy in the extended group is conjugacy in the affine Coxeter group. The Coxeter labels just computed are all even, so the odd-edge graph has three singleton components; by [F4] the three assigned positive parameters are constant on every required conjugacy class. In the symmetric convention the parameters are vs0=vs1=2 and vs2=3, with the quadratic relations of [F2].

3.1F2L1step 1.1step 1.2step 2.1∎

Here Y=Q∨, so the extended group has trivial length-zero quotient and Ω={1}. Applying [L1] to the affine Coxeter system identified in step 1.2, with the valid affine Coxeter parameters from step 2.1, shows that {Tw:w∈Waff} is a C-basis. This verifies the claimed unequal-parameter affine B2 example.

Coxeter diagram

The nodes label the three affine simple reflections. An edge labelled 4 means the product of the two reflections has order 4; no edge between s0 and s1 means their product has order 2. The node text records which walls are long-root and short-root walls.

s0s2s144longshortlong

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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