ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 quantum and Hecke operators commute in rank two

Example

Let $F = Q (q)$ , $N = 2$ , $V_{2} = F e_{1} \oplus F e_{2}$ , $K = L_{1} L_{2}^{- 1}$ , and $η = q - q^{- 1}$ . Write $e_{a} e_{b}$ for $e_{a} \otimes e_{b}$ . On $V_{2} \otimes V_{2}$ let $T$ be the ordered-basis operator and set

$E = E_{1} \otimes K + 1 \otimes E_{1}, F = F_{1} \otimes 1 + K^{- 1} \otimes F_{1} .$

The complete pair calculation is

Input	$E$	$T E$	$E T$	$F$	$T F$	$F T$
$e_{1} e_{1}$	$0$	$0$	$0$	$e_{2} e_{1} + q^{- 1} e_{1} e_{2}$	$e_{1} e_{2} + q e_{2} e_{1}$	$e_{1} e_{2} + q e_{2} e_{1}$
$e_{1} e_{2}$	$e_{1} e_{1}$	$q e_{1} e_{1}$	$q e_{1} e_{1}$	$e_{2} e_{2}$	$q e_{2} e_{2}$	$q e_{2} e_{2}$
$e_{2} e_{1}$	$q e_{1} e_{1}$	$q^{2} e_{1} e_{1}$	$q^{2} e_{1} e_{1}$	$q e_{2} e_{2}$	$q^{2} e_{2} e_{2}$	$q^{2} e_{2} e_{2}$
$e_{2} e_{2}$	$q^{- 1} e_{1} e_{2} + e_{2} e_{1}$	$e_{1} e_{2} + q e_{2} e_{1}$	$e_{1} e_{2} + q e_{2} e_{1}$	$0$	$0$	$0$

Also, $L_{1} \otimes L_{1}$ has diagonal entries $(q^{2}, q, q, 1)$ and $L_{2} \otimes L_{2}$ has entries $(1, q, q, q^{2})$ in this basis. Both commute with $T$ because $T$ preserves the multiset of the two labels.

Facts & Assumptions

Given: $F = Q (q)$ , the ordered basis $e_{1} < e_{2}$ , the type-A quantum generators and coproduct, and the operator $T$ .

[F1]

The pair operator fixes an equal pair with coefficient $q$ , flips an increasing pair, and adds $η$ times a decreasing pair (The ordered-basis Hecke operator and its normalization).

[F2]

The vector matrices satisfy $L_{j} e_{a} = q^{δ_{j a}} e_{a}$ , $E_{i} e_{a} = δ_{a, i + 1} e_{i}$ , and $F_{i} e_{a} = δ_{a, i} e_{i + 1}$ (The type-A quantum algebra and its tensor-action formulas).

[F3]

$K_{i} = L_{i} L_{i + 1}^{- 1}$ for $1 \leq i < N$ (The type-A quantum algebra and its tensor-action formulas).

[F4]

The coproduct values are $Δ (E_{1}) = E_{1} \otimes K_{1} + 1 \otimes E_{1}$ and $Δ (F_{1}) = F_{1} \otimes 1 + K_{1}^{- 1} \otimes F_{1}$ (The type-A quantum algebra and its tensor-action formulas); these assignments descend through the presentation (The type-A quantum presentation descends to its coproduct tensor action).

Verification

Given: The data in [F1]–[F4].

1.1givenF1F2F3F4algebra

From [F2]–[F3], $K_{1} e_{1} = q e_{1}$ and $K_{1} e_{2} = q^{- 1} e_{2}$ . Applying the two summands in [F4] to each of the four basis pairs gives the $E$ column in the displayed table; applying [F1] before or after those four outputs gives the two identical columns $T E$ and $E T$ . Hence $T E = E T$ on a basis and therefore on $V_{2} \otimes V_{2}$ .

1.2givenF1F2F3F4algebra

Using the same $K_{1}$ eigenvalues from [F2]–[F3], the two summands in [F4] give the four $F$ entries. Applying [F1] before or after them yields the equal columns $T F$ and $F T$ , so $T F = F T$ on the whole tensor square.

2.1givenF1F2algebra∎

On an input pair $(e_{a}, e_{b})$ , each $L_{j} \otimes L_{j}$ acts by $q^{δ_{j a} + δ_{j b}}$ by [F2]. Every term of $T (e_{a} \otimes e_{b})$ has the same multiset of labels by [F1], so the same scalar acts on every output term. This proves commutation with both $L_{1} \otimes L_{1}$ and $L_{2} \otimes L_{2}$ , and with their inverses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Pavel Etingof and Mykola Semenyakin, A brief introduction to quantum groups (standard reference, not scraped)
Li Luo and Weiqiang Wang, Lectures on dualities ABC in representation theory (standard reference, not scraped)