ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge 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 sl2 reciprocity matrices

Example

Assume the Axiom of Choice (The Axiom of Choice).

Let $g = {s l}_{2}$ and order the two labels of the regular integral block as $(0, - 2)$ . The standard-composition matrix $D$ has rows indexed by the Verma modules $Δ (0), Δ (- 2)$ and columns by the simples $L (0), L (- 2)$ , so $D = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array}) :$ $[Δ (0) : L (0)] = [Δ (0) : L (- 2)] = 1$ , $[Δ (- 2) : L (- 2)] = 1$ and $[Δ (- 2) : L (0)] = 0$ . The projective-flag matrix $F$ has rows indexed by the projective covers $P (0), P (- 2)$ and columns by the standards $Δ (0), Δ (- 2)$ , so $F = (\begin{array}{cc} 1 & 0 \\ 1 & 1 \end{array}) .$ Thus $F$ is the transpose of $D$ , which is the two-by-two instance of BGG reciprocity $(P (λ) : Δ (μ)) = [Δ (μ) : L (λ)]$ proved in BGG reciprocity.

Facts & Assumptions

Given: The Axiom of Choice, $g = {s l}_{2}$ , the regular integral block with labels $0, - 2$ , and its standards, simples and projective covers.

[F1]

The composition multiplicities of the two standards are $[Δ (0) : L (0)] = [Δ (0) : L (- 2)] = [Δ (- 2) : L (- 2)] = 1$ and $[Δ (- 2) : L (0)] = 0$ , because $Δ (0) = M (0)$ has the nonsplit composition series $L (- 2), L (0)$ and $Δ (- 2) = M (- 2) = L (- 2)$ (The two projectives in the principal sl2 block).

[F2]

The Verma-flag multiplicities of the two covers are $(P (0) : Δ (0)) = 1$ , $(P (0) : Δ (- 2)) = 0$ , $(P (- 2) : Δ (0)) = 1$ and $(P (- 2) : Δ (- 2)) = 1$ (The two projectives in the principal sl2 block, Finite Verma flags and their multiplicities).

[F3]

BGG reciprocity gives $(P (λ) : Δ (μ)) = [Δ (μ) : L (λ)]$ for all weights (BGG reciprocity).

Verification

technique · direct: read the two matrices off the sl2 computation and compare entries

1.1F1given

In the order $(0, - 2)$ the standard-composition matrix with entries $D_{λ μ} = [Δ (λ) : L (μ)]$ has rows indexed by the standards $λ = 0, - 2$ and columns indexed by the simples $μ = 0, - 2$ ; by [F1] its entries are $D_{00} = D_{0, - 2} = D_{- 2, - 2} = 1$ and $D_{- 2, 0} = 0$ , that is, $D = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ .

1.2F2given

In the same order the projective-flag matrix with entries $F_{λ μ} = (P (λ) : Δ (μ))$ has, by [F2], $F_{00} = 1$ , $F_{0, - 2} = 0$ , $F_{- 2, 0} = 1$ and $F_{- 2, - 2} = 1$ , that is, $F = (\begin{array}{cc} 1 & 0 \\ 1 & 1 \end{array})$ .

2.1F3step 1.1step 1.2algebra∎

By [F3] each entry of $F$ equals the transposed entry of $D$ : $F_{λ μ} = [Δ (μ) : L (λ)] = D_{μ λ}$ , so $F = D^{T}$ ; this is the two-by-two instance of BGG reciprocity, as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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, Theorem 2.2 with the rank-one computation (standard reference, not scraped)
Pavel Etingof, Representations of Lie Groups (18.757, Fall 2023), Sec. 20.2-20.3 (standard reference, not scraped)