ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 Hecke Jucys-Murphy elements through rank four

Example

Let $R$ be a commutative ring and $q \in R^{\times}$ . In $H = H_{R, q} (S_{n})$ the Hecke Jucys-Murphy elements (Hecke Jucys-Murphy elements and q-contents) for $n \geq 4$ are $L_{1} = 0, L_{2} = q^{- 1} T_{(1, 2)}, L_{3} = q^{- 1} T_{(2, 3)} + q^{- 2} T_{(1, 3)}, L_{4} = q^{- 1} T_{(3, 4)} + q^{- 2} T_{(2, 4)} + q^{- 3} T_{(1, 4)},$ and in general $L_{k} = \sum_{j < k} q^{j - k} T_{(j, k)}$ . For the standard tableau $t = \begin{matrix} 1 & 3 & 4 \\ 2 \end{matrix}$ of shape $(3, 1)$ the contents of the entries $k = 1, 2, 3, 4$ are $0, - 1, 1, 2$ (The content of a node and the content vector of a standard tableau), so the diagonal eigenvalues of $L_{1}, \dots, L_{4}$ on the Murphy vector $m_{t}$ are $[0]_{q} = 0$ , $[- 1]_{q} = - q^{- 1}$ , $[1]_{q} = 1$ and $[2]_{q} = 1 + q$ ; the triangular correction terms $\sum_{v ⊳ t} a_{v} m_{v}$ are present in general (The Hecke Jucys-Murphy action is dominance triangular) in the Murphy basis, even in the semisimple range. In the separated range, replacing $m_{t}$ by the seminormal vector $f_{t}$ removes these correction terms, as proved in Separated Hecke residues give seminormal idempotents and bases. At $q = 1$ the four elements specialize to the ordinary Jucys-Murphy elements $X_{1} = 0$ , $X_{2} = (1 2)$ , $X_{3} = (1 3) + (2 3)$ , $X_{4} = (1 4) + (2 4) + (3 4)$ and the eigenvalues to $0, - 1, 1, 2$ , the standard contents of $t$ .

Facts & Assumptions

Given: A commutative ring $R$ , $q \in R^{\times}$ , the Hecke algebra $H_{R, q} (S_{n})$ , the Jucys-Murphy elements and q-contents (Hecke Jucys-Murphy elements and q-contents), the content vector of a standard tableau (The content of a node and the content vector of a standard tableau), and the q=1 specialization $H_{R, 1} (S_{n}) ≅ R [S_{n}]$ (Hecke Jucys-Murphy elements and q-contents).

[F1]

(Hecke Jucys-Murphy elements and q-contents) $L_{k} = \sum_{j < k} q^{j - k} T_{(j, k)}$ ; $[m]_{q} = 1 + q + \dots + q^{m - 1}$ for $m \geq 0$ , $[- m]_{q} = - q^{- m} [m]_{q}$ for $m > 0$ , and $[m]_{1} = m$ for all $m \in Z$ .

[F2]

(The Hecke Jucys-Murphy action is dominance triangular) $m_{t} L_{k} = [{content}_{t} (k)]_{q} m_{t} + \sum_{v ⊳ t} a_{v} m_{v}$ on the Murphy cell module, so the displayed values are the diagonal entries and the correction terms are as stated.

Verification

1.1givenF1

Substitution: in [F1], for $k = 1$ the sum is empty, giving $L_{1} = 0$ ; for $k = 2$ it has the single term $q^{1 - 2} T_{(1, 2)} = q^{- 1} T_{(1, 2)}$ ; for $k = 3$ it has $q^{- 1} T_{(2, 3)} + q^{- 2} T_{(1, 3)}$ ; and for $k = 4$ it has $q^{- 1} T_{(3, 4)} + q^{- 2} T_{(2, 4)} + q^{- 3} T_{(1, 4)}$ , matching the displayed list.

1.2givenF1

Contents: reading the tableau $t$ with rows $(1, 3, 4)$ and $(2)$ , the node of $1$ is $(1, 1)$ with content $1 - 1 = 0$ , the node of $2$ is $(2, 1)$ with content $1 - 2 = - 1$ , the node of $3$ is $(1, 2)$ with content $2 - 1 = 1$ and the node of $4$ is $(1, 3)$ with content $3 - 1 = 2$ ; by definition $[{content}_{t} (k)]_{q}$ is the q-integer of these contents.

2.1step 1.1step 1.2F1F2

Eigenvalues: by [F1], $[0]_{q} = 0$ , $[- 1]_{q} = - q^{- 1} [1]_{q} = - q^{- 1}$ , $[1]_{q} = 1$ and $[2]_{q} = 1 + q$ ; substituting into the triangularity formula [F2] gives the stated diagonal eigenvalues $0, - 1, 1, 2$ up to the q-powers $- q^{- 1}, 1, 1 + q$ . The correction terms are exactly the sum $\sum_{v ⊳ t} a_{v} m_{v}$ of [F2] and are not asserted to vanish outside the semisimple range.

3.1step 1.2step 2.1F1∎

Specialization: setting $q = 1$ in the displayed formulas turns $L_{k}$ into $\sum_{j < k} (j k) = X_{k}$ by the specialization isomorphism of Hecke Jucys-Murphy elements and q-contents and [F1], giving $X_{1} = 0$ , $X_{2} = (1 2)$ , $X_{3} = (1 3) + (2 3)$ and $X_{4} = (1 4) + (2 4) + (3 4)$ ; the eigenvalues $[m]_{1} = m$ become $0, - 1, 1, 2$ , the contents of $t$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Andrew Mathas, Hecke algebras and Schur algebras of the symmetric group, complete prepublication manuscript (1998; expanded published edition: AMS University Lecture Series 15, 1999); complete 79-page manuscript, SHA-256 8cfeb611a95a3ff25cb95ad22bfd3a68475818301c34b04d131a8480a1b997e0 (standard reference, not scraped)