ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-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 small parabolic category O character formula

Example

For ${s l}_{3}$ , $λ = 0$ , $J = {s_{1}}$ , the genuine regular parabolic category has minimal-left labels $(e, s_{2}, s_{2} s_{1})$ , with highest weights $0, - α_{2}, - α_{1} - 2 α_{2}$ . Its generalized-standard/simple matrix is $N = (\begin{array}{ccc} 1 & 1 & 0 \\ 0 & 1 & 1 \\ 0 & 0 & 1 \end{array}), N^{- 1} = (\begin{array}{ccc} 1 & - 1 & 1 \\ 0 & 1 & - 1 \\ 0 & 0 & 1 \end{array}) .$ Thus $ch L (0) = ch Δ^{J} (0) - ch Δ^{J} (- α_{2}) + ch Δ^{J} (- α_{1} - 2 α_{2}),$ $ch L (- α_{2}) = ch Δ^{J} (- α_{2}) - ch Δ^{J} (- α_{1} - 2 α_{2})$ , and $ch L (- α_{1} - 2 α_{2}) = ch Δ^{J} (- α_{1} - 2 α_{2})$ .

For comparison retain the singular antidominant block with $μ + ρ = - ω_{2}$ and right-minimal labels $(e, s_{2}, s_{1} s_{2})$ : its composition matrix $A = (\begin{array}{ccc} 1 & 0 & 0 \\ 1 & 1 & 0 \\ 1 & 1 & 1 \end{array})$ has inverse $(\begin{array}{ccc} 1 & 0 & 0 \\ - 1 & 1 & 0 \\ 0 & - 1 & 1 \end{array})$ , giving $ch L (μ) = ch M (μ)$ , $ch L (s_{2} \cdot μ) = ch M (s_{2} \cdot μ) - ch M (μ)$ , and $ch L (s_{1} s_{2} \cdot μ) = ch M (s_{1} s_{2} \cdot μ) - ch M (s_{2} \cdot μ)$ . The latter coefficients are Mobius values in this all-one singular chain only. The two blocks exemplify distinct spherical and antispherical formulas; the singular example is not the generalized-Verma character formula of the parabolic category.

Facts & Assumptions

Given: The ${s l}_{3}$ data: dominant regular $λ = 0$ and $J = {s_{1}}$ for the parabolic block; $μ$ with $μ + ρ = - ω_{2}$ for the singular block; the label sets $^{J} W = (e, s_{2}, s_{2} s_{1})$ and $W^{J} = (e, s_{2}, s_{1} s_{2})$ (Parabolic category O for a standard parabolic, The singular integral block and its dot stabilizer).

[F1]

Regular parabolic multiplicities: $[Δ^{J} (y \cdot λ) : L (x \cdot λ)] = n_{y, x} (1)$ for $x, y \in^{J} W$ (Parabolic category O multiplicities are parabolic Kazhdan–Lusztig values), and the character formula $ch L (x \cdot λ) = \sum_{y \geq x} (N^{- 1})_{x, y} ch Δ^{J} (y \cdot λ)$ with $N = (n_{y, x} (1))$ (The parabolic Kazhdan–Lusztig character formula).

[F2]

The $S_{3}$ antispherical values $n_{y, x} (1)$ of Parabolic Kazhdan–Lusztig polynomials for S_3 modulo S_2 in the order $(e, s_{2}, s_{2} s_{1})$ are the matrix $N$ displayed above; its inverse is the integer matrix displayed (verified by the two matrix products in the Verification below).

[F3]

Singular multiplicities: in the singular block of $μ$ with $y, w \in W^{J} = (e, s_{2}, s_{1} s_{2})$ , $[M (y \cdot μ) : L (w \cdot μ)] = P_{y w_{0}, w w_{0}} (1) = 1$ exactly for $y \geq w$ and $0$ otherwise (Singular category O multiplicities are parabolic Kazhdan–Lusztig values, Translation to a singular wall in type A_2); BGG reciprocity gives the projective version (BGG reciprocity).

[F4]

Grothendieck-group and inversion data: the simple and generalized-standard classes are bases, characters are injective, and inverse matrices are computed by the finite signed chain inversions of the unitriangular multiplicity matrix (Parabolic category O is a highest weight category (4) for generalized standards, The Grothendieck group and character of O, Simple and standard bases of K0(O) for ordinary standards, and Inverse Kazhdan–Lusztig polynomials, The Kazhdan–Lusztig inversion formula for the ordinary inverse comparison).

[F5]

The parabolic highest weights: $e \cdot 0 = 0$ , $s_{2} \cdot 0 = - α_{2}$ , $s_{2} s_{1} \cdot 0 = - α_{1} - 2 α_{2}$ , and the singular labels for $W^{J}$ are $μ$ , $s_{2} \cdot μ$ , $s_{1} s_{2} \cdot μ$ with the dominance chain of Translation to a singular wall in type A_2.

Verification

technique · direct finite matrix inversion in the two blocks, with the two products checked entrywise

1.1F2algebra

The parabolic matrix. By [F2] the matrix $N = (n_{y, x} (1))$ in the order $(e, s_{2}, s_{2} s_{1})$ is the displayed upper unitriangular matrix. The displayed matrix $N^{- 1}$ is its inverse: $N N^{- 1}$ has entries $\sum_{z} n_{y, z} (1) (N^{- 1})_{z, x}$ , which equal $1$ for $y = x$ and $0$ otherwise (the only nonzero contributions are from $z \in {y, \dots, x}$ with the alternating coefficients), and similarly $N^{- 1} N = I$ . Both products are finite integer calculations.

1.2F3algebra

The singular matrix. By [F3] the composition matrix in the order $(e, s_{2}, s_{1} s_{2})$ is $A = (\begin{array}{ccc} 1 & 0 & 0 \\ 1 & 1 & 0 \\ 1 & 1 & 1 \end{array})$ (entry $(y, w)$ is $1$ exactly when $y \geq w$ ). The displayed matrix $B = (\begin{array}{ccc} 1 & 0 & 0 \\ - 1 & 1 & 0 \\ 0 & - 1 & 1 \end{array})$ satisfies $A B = I = B A$ by the same finite chain computation, so $A^{- 1} = B$ .

2.1F1F5step 1.1algebra

The parabolic characters. By [F1] and step 1.1, $ch L (x \cdot λ) = \sum_{y} (N^{- 1})_{x, y} ch Δ^{J} (y \cdot λ)$ . Reading the rows of $N^{- 1}$ in the order $(e, s_{2}, s_{2} s_{1})$ gives exactly the three displayed character identities, using $0$ , $- α_{2}$ , $- α_{1} - 2 α_{2}$ as the labels of $e \cdot 0$ , $s_{2} \cdot 0$ , $s_{2} s_{1} \cdot 0$ by [F5]: with $ρ = α_{1} + α_{2}$ , the type- $A_{2}$ reflection relations give $s_{2} ρ = α_{1}$ and $s_{2} s_{1} ρ = - α_{2}$ , hence the stated dot translates after subtracting $ρ$ .

3.1F1F3F4step 1.1step 2.1step 1.2algebra∎

The singular characters and the comparison. By [F3] and [F4], $ch L (w \cdot μ) = \sum_{y} (A^{- 1})_{w, y} ch M (y \cdot μ)$ ; the rows of $B = A^{- 1}$ give the three displayed singular identities, in which the nonzero off-diagonal coefficients are the Mobius values $\pm 1$ of this all-one chain only. The parabolic coefficients of step 2.1 include the value $+ 1$ in the $(1, 3)$ position of $N^{- 1}$ , which the singular inverse does not have: the two formulas are different character formulas for different blocks, and the singular one is not the generalized-Verma character formula of the parabolic category.

Remarks

The example is the smallest case in which both inversions can be written down explicitly: the spherical/antispherical distinction of the companion counterexample persists in the inverse matrices, and no singular/parabolic category equivalence or grading is used. The two blocks have different label orders (left-minimal versus right-minimal representatives), which is why both index dictionaries are displayed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

82 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

Lin Chen, lecture notes (Spring 2024), Lecture 9: standard filtrations, BGG reciprocity and translation functors (complete 7-page lecture) (standard reference, not scraped)
Anders Bjoerner and Francesco Brenti, Combinatorics of Coxeter Groups, Graduate Texts in Mathematics 231, Springer 2005 (author-hosted complete 370-page PDF) (standard reference, not scraped)
Anne Moreau, M2 Representation Theory 2025–2026 (current complete 129-page author notes) (standard reference, not scraped)