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

A B2 unequal-parameter KL basis and four left-cell transitions

Example

Let $W = I_{2} (4) = ⟨ s, t ∣ s^{2} = t^{2} = 1, (s t)^{4} = 1 ⟩$ , and put $L (s) = 1$ , $L (t) = 2$ . In $H_{A} (W, L)$ , with $A = Z [v, v^{- 1}]$ , set $C_{s} = T_{s} + v^{- 1}, C_{t} = T_{t} + v^{- 2} .$ Then $C_{s t} = C_{s} C_{t} = T_{s t} + v^{- 2} T_{s} + v^{- 1} T_{t} + v^{- 3}, C_{t s} = C_{t} C_{s} = T_{t s} + v^{- 1} T_{t} + v^{- 2} T_{s} + v^{- 3}, C_{s}^{2} = (v + v^{- 1}) C_{s}, C_{t}^{2} = (v^{2} + v^{- 2}) C_{t} .$ The cell convention is that $x \leftarrow_{L} y$ when $C_{x}$ has nonzero coefficient in $C_{r} C_{y}$ for some $r \in {s, t}$ ; the diagram below uses a directed edge $y \to x$ for this transition. It records the four transitions $1 \to s$ , $1 \to t$ , $s \to t s$ , and $t \to s t$ . It does not assert a complete classification of the $I_{2} (4)$ cells.

The top edge is the Coxeter graph, labelled by its braid length. In the lower directed graph, an edge labelled $C_{r} \cdot$ means left multiplication by $C_{r}$ ; the source is $y$ , the target is $x$ , and $C_{x}$ has coefficient $1$ in the product $C_{r} C_{y}$ . The equations in the proof establish each edge directly, so the diagram is only a summary.

Facts & Assumptions

Given: The Coxeter system $I_{2} (4)$ , the weights $L (s) = 1, L (t) = 2$ , and the weighted KL and cell conventions in the Statement.

[F1]

Arbitrary-rank Coxeter presentations, length, reflections, and Bruhat order, Finite-generator standard parabolics and the Bruhat subword property at arbitrary rank, and Simple-generator weights extend uniquely to a weight function: the Coxeter presentation defines length and Bruhat order; finite-generator parabolics preserve lengths and Bruhat order has the reduced-subword description; simple labels extend exactly when finite odd edges have equal labels.

[F2]

The unequal-parameter Coxeter Hecke algebra and The arbitrary-rank weighted Hecke basis and Bruhat-triangular bar: the quadratic relation is $T_{r}^{2} = (v^{L (r)} - v^{- L (r)}) T_{r} + 1$ , and the standard elements form a basis.

[F3]

Existence and uniqueness of the ordered-group unequal-parameter Kazhdan–Lusztig basis: the KL basis is the unique bar-invariant basis triangular below Bruhat order, with negative-exponent lower coefficients and the stated positive-weight simple-generator normalization.

[F4]

Unequal-parameter left, right, and two-sided cells and cell quotients: $x \leftarrow_{L} y$ exactly when the coefficient of $C_{x}$ in $C_{r} C_{y}$ is nonzero for a simple generator $r$ .

Verification

Given: The data in the Statement.

1.1F1algebra

Since $m (s, t) = 4$ is even, the weight extension criterion [F1] permits $L (s) = 1, L (t) = 2$ . Put $r = s t$ . The presentation gives $t = s r$ and $s r s = t s = r^{- 1}$ . Hence every word is $r^{j}$ or $r^{j} s$ for some $j \in {0, 1, 2, 3}$ , so $∣ W ∣ \leq 8$ . Map $s$ to reflection across the horizontal axis and $t$ to reflection across the diagonal $y = x$ . Their product is a rotation by $90$ degrees, so these transformations generate all eight symmetries of the square and define a surjection from $W$ onto that group. Thus $W$ is that dihedral group. In particular $1, s, t, s t, t s$ are distinct; $s, t$ have length one and $s t, t s$ length two. The reduced-subword theorem [F1] then gives the lower intervals below $s t$ and $t s$ as ${1, s, t, s t}$ and ${1, s, t, t s}$ .

2.1F1F2F3step 1.1algebra

By [F3], $C_{s} = T_{s} + v^{- 1}$ and $C_{t} = T_{t} + v^{- 2}$ . Expanding in the standard basis [F2] gives $C_{s} C_{t} = T_{s t} + v^{- 2} T_{s} + v^{- 1} T_{t} + v^{- 3}$ . Each lower term is indexed by a strict Bruhat subword from step 1.1 and has negative exponent. Since $C_{s}, C_{t}$ are bar invariant, their product is bar invariant; uniqueness in [F3] identifies it with $C_{s t}$ . Reversing the product gives $C_{t} C_{s} = T_{t s} + v^{- 1} T_{t} + v^{- 2} T_{s} + v^{- 3} = C_{t s}$ .

3.1F2F3F4step 2.1algebra∎

The quadratic relation gives $C_{s}^{2} = T_{s}^{2} + 2 v^{- 1} T_{s} + v^{- 2} = (v + v^{- 1}) T_{s} + 1 + v^{- 2} = (v + v^{- 1}) C_{s}$ . Using $L (t) = 2$ gives $C_{t}^{2} = (v^{2} + v^{- 2}) C_{t}$ . Also $C_{s} C_{1} = C_{s}$ , $C_{t} C_{1} = C_{t}$ , $C_{t} C_{s} = C_{t s}$ , and $C_{s} C_{t} = C_{s t}$ . By [F4], these products give the four directed transitions displayed in the Statement and diagram. The proof establishes only these edges and makes no claim that the list is exhaustive.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

George Lusztig, Hecke Algebras with Unequal Parameters, revised arXiv text (2014) (standard reference, not scraped)
Anders Björner and Francesco Brenti, Combinatorics of Coxeter Groups, GTM 231 (2005) (standard reference, not scraped)