TheoremStatement: Literature-sourcedProof: 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.

The good node gives the simple socle and head of the residue restriction

Statement

Let $k$ be a field of characteristic $p > 0$ , $μ$ a $p$ -restricted partition of $d$ and $i \in Z / p$ with $ε_{i} (μ) > 0$ ; let $A$ be the good $i$ -node and $ν = μ ∖ A$ (Residue signatures, normal, good, conormal and cogood nodes). For the residue-summand functor $E_{i}$ of Generalized Jucys-Murphy primary idempotents and the residue-summand functors $E_{i}$ , $F_{i}$ the module $E_{i} D (μ)$ has simple socle and simple head, both isomorphic to $D (ν)$ , and the total (ungraded) multiplicity of $D (ν)$ in $E_{i} D (μ)$ is $ε_{i} (μ)$ . Thus the Loewy endpoints are simple even though the formal character of $E_{i} D (μ)$ may contain the additional normal-node factors of Normal-node composition multiplicities under residue restriction.

Facts & Assumptions

Given: A field $k$ of characteristic $p > 0$ , a $p$ -restricted partition $μ$ of $d$ , a residue $i$ with $ε_{i} (μ) > 0$ , the good $i$ -node $A$ and $ν = μ ∖ A$ .

[F1]

Kleshchev's uncoloured socle theorem in its residue-refined form (The socle of an uncoloured modular restriction is the multiplicity-free sum over the good residues): ${soc}_{S_{d - 1}} (D (μ) ↓_{S_{d - 1}}) = ⨁_{j : ε_{j} (μ) > 0} D (μ ∖ A_{j}),$ a multiplicity-free sum over the good nodes, one per residue with $ε_{j} (μ) > 0$ .

[F2]

$Res D (μ) = ⨁_{j} E_{j} D (μ)$ is a direct sum of $k S_{d - 1}$ -submodules. If $X$ is a removable $i$ -node of $μ$ , $μ ∖ X$ is $p$ -restricted, and $D (μ ∖ X)$ occurs as a composition factor of the restriction, then every occurrence belongs to the summand $E_{i} D (μ)$ with $res (X) = i$ (Generalized Jucys-Murphy primary idempotents and the residue-summand functors $E_{i}$ , $F_{i}$ ); the localization is proved in Normal-node composition multiplicities under residue restriction.

[F3]

The normal-node multiplicity theorem (Normal-node composition multiplicities under residue restriction): if $X$ is a removable $i$ -node of $μ$ with $μ ∖ X$ $p$ -restricted, then $[E_{i} D (μ) : D (μ ∖ X)]$ is the number of normal $i$ -nodes of $μ$ weakly below $X$ (counting $X$ ) when $X$ is normal, and $0$ otherwise.

[F4]

$D (μ)$ is self-dual for $p$ -restricted $μ$ , and the functor $E_{i}$ commutes with contragredient duality, so $E_{i} D (μ)$ is self-dual; and $D (ν)$ is simple, self-dual and absolutely irreducible (p-regular and p-restricted labels under transpose and sign, Generalized Jucys-Murphy primary idempotents and the residue-summand functors $E_{i}$ , $F_{i}$ ).

[F5]

For a finite-dimensional module $M$ : $soc M$ is the sum of its simple submodules, the socle of a direct sum is the direct sum of the socles of its summands, and the head of a self-dual module is the dual of its socle, $hd M ≅ (soc M)^{*}$ (The radical, socle, head, and Loewy series of a finite-dimensional module).

[F6]

The good $i$ -node is the topmost normal $i$ -node, so the normal $i$ -nodes weakly below it are exactly all normal $i$ -nodes of $μ$ , and there are $ε_{i} (μ)$ of them (Residue signatures, normal, good, conormal and cogood nodes).

Proof

technique · direct

1.1givenF1F2F5

Socle. By [F5] the socle of $Res D (μ) = ⨁_{j} E_{j} D (μ)$ is $⨁_{j} soc (E_{j} D (μ))$ . By [F1] the socle of the restriction is the multiplicity-free sum of the $D (μ ∖ A_{j})$ over the good nodes, and by [F2] each summand $D (μ ∖ A_{j})$ lies in $E_{j} D (μ)$ with its residue $j$ ; since a nonzero submodule of $E_{j} D (μ)$ cannot lie in $⨁_{l \neq j} E_{l} D (μ)$ by the directness of the sum, the $j$ -summand of the socle is exactly the single simple module $D (μ ∖ A_{j})$ and $soc (E_{j} D (μ)) = D (μ ∖ A_{j})$ is simple. For $j = i$ this gives $soc (E_{i} D (μ)) = D (μ ∖ A) = D (ν)$ .

2.1step 1.1F3F6

Multiplicity. Applying the normal-node theorem [F3] with $X = A$ : since $A$ is a normal $i$ -node, $[E_{i} D (μ) : D (ν)]$ is the number of normal $i$ -nodes of $μ$ weakly below $A$ counting $A$ ; by [F6] this is $ε_{i} (μ)$ .

2.2step 1.1F4F5

Head. By [F4] the module $E_{i} D (μ)$ is self-dual; by [F5] its head is the dual of its socle, $hd (E_{i} D (μ)) ≅ (soc (E_{i} D (μ)))^{*}$ , which by step 1.1 is $D (ν)^{*} ≅ D (ν)$ because $D (ν)$ is self-dual by [F4]. Hence the head is simple and isomorphic to $D (ν)$ .

3.1step 1.1step 2.1step 2.2∎

Conclusion. Step 1.1 gives simple socle $D (ν)$ , step 2.1 the total multiplicity $ε_{i} (μ)$ of $D (ν)$ in $E_{i} D (μ)$ , and step 2.2 simple head $D (ν)$ . The additional normal-node composition factors of [F3] may occur in the middle Loewy layers; the statement asserts only the endpoints and the total multiplicity, and no graded shift is displayed before the Hecke/KLR bridge.

Remarks

Where each input is used. The simple socle and the identification of its label come from the recorded uncoloured socle theorem and the localization of the factor in its residue summand; the multiplicity $ε_{i} (μ)$ is the normal-node count at the good node, and self-duality produces the head. No complex character theory is used.
Distinct statements. The Hom criterion for Specht modules and the socle theorem beyond the good-node summands are not asserted here.

Depends on

Used by

Dependency tree · two levels

36 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.