CorollaryStatement: AI-adaptedProof: 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 restricted graded Specht classes form a basis of the module Grothendieck group

Statement

In the stated nondegenerate level-one regime and each residue content $α$ , the classes $[S (λ)]$ indexed by RESTRICTED shapes $λ$ form an $A$ -basis of $G_{0}^{g r} (H_{α})$ . Under $Ψ_{c a n}$ they correspond to the restricted standard coordinate functionals ${Std}_{λ} = π (M_{λ})$ , which form an $A$ -basis of the UPPER integral dual lattice. Separately, all raw standard $M_{μ}$ of that content form an $A$ -basis of the ambient Fock standard lattice; their full projected family is generally redundant. No claim that ${Std}_{λ}$ is a basis of the lower lattice or that the field Gram denominator is an $A$ -unit is made. Choice only as inherited.

Facts & Assumptions

Given: The nondegenerate level-one regime, a residue content $α$ , the graded Specht modules $S (λ)$ for restricted shapes, and the transported identification $Ψ_{c a n}^{H e c k e}$ .

[F1]

The transported identification sends $[S (μ)]$ to the standard monomial image $S_{μ} = π (M_{μ})$ for every partition $μ$ (Graded Specht classes realize the standard Fock vectors); at restricted shapes these are the restricted standard coordinate functionals ${Std}_{λ}$ of Standard Fock vectors expand in the upper global basis.

[F2]

The restricted coordinate functionals form an $A$ -basis of the upper dual lattice, by the dominance-unitriangular restricted coefficient minor, while the raw standard vectors form the ambient standard lattice basis and the projected family is generally redundant (Standard Fock vectors expand in the upper global basis).

[F3]

The map $Ψ_{c a n}^{H e c k e} : G_{0}^{g r} (H^{Λ}) \to V_{A} (Λ_{0})^{\lor}$ is an $A$ -module isomorphism onto the restricted integral weight dual, carrying normalized simple classes to the form-dual projective basis (The QG-8 categorification transports across the blockwise Hecke-KLR bridge); the graded module group is the restricted direct sum of the blockwise groups (Graded module and projective Grothendieck groups of the KLR and Hecke towers).

[F4]

The restricted labels are the $e$ -restricted partitions of the content, with the dominance-unitriangular transition polynomials of Level-one global-basis transition polynomials in the symmetric-group convention and The basic representation global basis is unitriangular in the partition basis; the regime is the one of The nondegenerate root-of-unity level-one Hecke regime.

[C1]

Choice is inherited only through the declared global-basis suppliers; the finite unitriangular matrix inversion introduces none (The Axiom of Choice, The QG-8 categorification transports across the blockwise Hecke-KLR bridge).

Proof

technique · direct

1.1F1F2

The image of the restricted classes. By [F1] the isomorphism $Ψ_{c a n}^{H e c k e}$ sends each class $[S (λ)]$ with $λ$ restricted to the coordinate functional ${Std}_{λ} = π (M_{λ})$ ; this is exactly the restricted family of [F2].

1.2F2F3F4

The ambient family and the boundaries of the claim. The raw standard vectors $M_{μ}$ are the ambient standard basis by [F2], and the full projected family ${{Std}_{μ}}$ is generally redundant; in particular the corollary does not assert that ${Std}_{λ}$ lies in or spans the lower lattice, nor that the Gram denominator $1 + q^{2}$ of the $e = 2$ example is an $A$ -unit [F2, F4]. All content weight spaces are finite, so the basis statements are componentwise finite [F3].

2.1F2F3step 1.1

Basis of the upper dual. The restricted family ${{Std}_{λ}}$ is an $A$ -basis of the upper dual lattice by [F2], and $Ψ_{c a n}^{H e c k e}$ is an isomorphism onto that lattice by [F3]; pulling this basis back gives that the classes $[S (λ)]$ with $λ$ restricted form an $A$ -basis of $G_{0}^{g r} (H_{α})$ [F3].

3.1C1F2given∎

Choice. The argument uses the inherited global-basis interfaces and one finite unitriangular matrix inversion per content; no family of nonempty sets is selected, so choice is inherited only as in [C1].

Depends on

Used by

Dependency tree · two levels

64 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

Jonathan Brundan and Alexander Kleshchev, Graded decomposition numbers for cyclotomic Hecke algebras, arXiv:0901.4450v3, Adv. Math. 222 (2009) 1883-1942 (complete 57-page article) (standard reference, not scraped)
Alexander Kleshchev, Representation theory of symmetric groups and related Hecke algebras, arXiv:0909.4844v1, Bull. Amer. Math. Soc. 47 (2010) 419-481 (complete 66-page survey) (standard reference, not scraped)