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

The eight PBW words at level two and rank two

Example

For $r = n = 2$ over $R = Z [Q^{\pm 1}, u_{1}^{\pm 1}, u_{2}^{\pm 1}]$ , the Ariki–Koike PBW basis is

${1, X_{1}, X_{2}, X_{1} X_{2}, T_{1}, X_{1} T_{1}, X_{2} T_{1}, X_{1} X_{2} T_{1}} .$

The relations include $X_{1}^{2} = (u_{1} + u_{2}) X_{1} - u_{1} u_{2}$ , $T_{1}^{2} = (Q - 1) T_{1} + Q$ , and $X_{2} = Q^{- 1} T_{1} X_{1} T_{1}$ .

Facts & Assumptions

Given: The multiplicative cyclotomic presentation and the Ariki–Koike PBW theorem over $R$ .

[F1]

The multiplicative cyclotomic Hecke algebra: $(T_{1} - Q) (T_{1} + 1) = 0$ .

[F2]

The multiplicative cyclotomic Hecke algebra: the affine relation is $T_{1} X_{1} T_{1} = Q X_{2}$ .

[F3]

The multiplicative cyclotomic Hecke algebra: the level-two cyclotomic relation is $(X_{1} - u_{1}) (X_{1} - u_{2}) = 0$ .

[F4]

The Ariki–Koike PBW basis and generic splitness: $X_{1}^{a_{1}} X_{2}^{a_{2}} T_{w}$ , $0 \leq a_{1}, a_{2} < 2$ , $w \in S_{2}$ , is an $R$ -basis.

Verification

Given: $r = n = 2$ , the generators $X_{1}, X_{2}, T_{1}$ , and the ordered PBW family from the example.

1.1F1F2F3algebra

Expanding the level-two cyclotomic polynomial [F3] gives $X_{1}^{2} = (u_{1} + u_{2}) X_{1} - u_{1} u_{2}$ . Expanding the Hecke quadratic [F1] gives $T_{1}^{2} = (Q - 1) T_{1} + Q$ , and the affine relation [F2] gives $X_{2} = Q^{- 1} T_{1} X_{1} T_{1}$ because $Q$ is a unit.

1.2givenalgebra

The exponent pairs $(a_{1}, a_{2}) \in {0, 1}^{2}$ give $1, X_{1}, X_{2}, X_{1} X_{2}$ , and $S_{2} = {1, s_{1}}$ gives the two right factors $1, T_{1}$ . Their eight products are exactly the displayed list.

2.1F1F2F3F4step 1.1step 1.2∎

The basis theorem [F4] applies with these values of $r, n$ and declares this enumerated PBW family an $R$ -basis. The relations in step 1.1 are the corresponding reductions in this presentation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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