PropositionStatement: AI-adaptedProof: 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 core-quotient size formula defines the weight

Statement

Let $e \geq 2$ and let $λ ⊢ n$ with $e$ -core $C_{e} (λ)$ and $e$ -weight $w_{e} (λ) = ∣ Q_{e} (λ) ∣$ (The e-core, the e-quotient, and the e-weight). Then $n = ∣ λ ∣ = ∣ C_{e} (λ) ∣ + e w_{e} (λ),$ so $w_{e} (λ) = (n - ∣ C_{e} (λ) ∣) / e \in N_{0}$ . Equivalently every sequence of removals of removable border strips of size $e$ from $λ$ down to its $e$ -core (The e-core is independent of the rim hook removal order) has exactly $w_{e} (λ)$ steps, and $w_{e} (λ) = ∣ Q_{e} (λ) ∣$ equals both the number of hooks of the multipartition $Q_{e} (λ)$ and, by the bijection of The e-quotient controls the hooks of e-divisible length, the number of hooks of $λ$ of length divisible by $e$ .

Throughout the proof, $λ ∖ H$ means deletion of the rim strip corresponding to the node hook $H$ , as in The e-quotient controls the hooks of e-divisible length.

No choice principle is used.

Facts & Assumptions

Given: An integer $e \geq 2$ and a partition $λ ⊢ n$ with $e$ -quotient $Q_{e} (λ) = (λ^{(0)}, \dots, λ^{(e - 1)})$ , $e$ -core $C_{e} (λ)$ and $e$ -weight $w_{e} (λ) = \sum_{i} ∣ λ^{(i)} ∣$ (The e-core, the e-quotient, and the e-weight).

[F1]

$C_{e} (λ)$ is well defined and is the terminal partition of every maximal sequence of removals of removable border strips of size $e$ from $λ$ ; each removed strip has size exactly $e$ and the terminal partition contains no hook of length $e$ (The e-core is independent of the rim hook removal order).

[F2]

There is a bijection $f$ from the hooks of $λ$ of $e$ -divisible length onto the hooks of the multipartition $Q_{e} (λ)$ with $∣ H ∣ = e ∣ f (H) ∣$ and $Q_{e} (λ ∖ H) = Q_{e} (λ) ∖ f (H)$ , where the latter removes the hook $f (H)$ from its component (The e-quotient controls the hooks of e-divisible length).

[F3]

For a partition $μ$ , the number of hooks of $μ$ equals $∣ μ ∣$ , since each box is the anchor of exactly one hook of $[μ]$ (Hook, arm, leg, and hook length of a box); a nonempty partition has a removable box, that is, a hook of size $1$ (Removable and addable nodes); and a hook of the multipartition $Q_{e} (λ)$ has the size of the corresponding hook of the component $λ^{(i)}$ (The e-core, the e-quotient, and the e-weight, The e-quotient controls the hooks of e-divisible length).

Proof

technique · induction on $w_e(\lambda)$

1.1F2F3

We first record the counting consequences of the quotient theorem. A hook of $λ$ has $e$ -divisible length exactly when it is the preimage under the bijection $f$ of [F2] of a hook of $Q_{e} (λ)$ , and the number of hooks of a partition equals its size by [F3]; hence the number of $e$ -divisible hooks of $λ$ equals the total size $w_{e} (λ) = \sum_{i} ∣ λ^{(i)} ∣$ of $Q_{e} (λ)$ . In particular $Q_{e} (λ)$ has a hook if and only if $w_{e} (λ) > 0$ , and then some hook has size $1$ by [F3], so $λ$ has a hook of length $e$ .

2.1F1basestep 1.1

Base case: if $w_{e} (λ) = 0$ then $Q_{e} (λ)$ has no hook by step 1.1, so $λ$ has no hook of $e$ -divisible length, hence no hook of length $e$ ; by [F1] the terminal partition of the empty removal sequence is $λ$ itself, that is, $C_{e} (λ) = λ$ , and the removal sequence has $0 = w_{e} (λ)$ steps.

2.2F1F2F3step 1.1

Induction step: let $w_{e} (λ) > 0$ . By step 1.1 there is a hook $H$ of $λ$ of length exactly $e$ , a removable border strip of size $e$ by [F1]. By the removal identity of [F2], $Q_{e} (λ ∖ H) = Q_{e} (λ) ∖ f (H),$ and since $f (H)$ is a hook of a component of $Q_{e} (λ)$ of size $∣ H ∣ / e = 1$ , the right-hand side is the multipartition obtained by deleting one box, so by [F3] its size is $w_{e} (λ) - 1$ . Moreover $C_{e} (λ ∖ H) = C_{e} (λ)$ : a maximal sequence from $λ ∖ H$ is the tail of a maximal sequence from $λ$ beginning with $H$ , and all maximal sequences from $λ$ end at $C_{e} (λ)$ by [F1].

3.1F1IHstep 2.1step 2.2algebra

By step 2.2 we may apply the induction hypothesis to $λ ∖ H$ , whose weight is $w_{e} (λ) - 1 < w_{e} (λ)$ : every maximal sequence of $e$ -strip removals from $λ ∖ H$ has $w_{e} (λ) - 1$ steps and $∣ λ ∣ - e = ∣ λ ∖ H ∣ = ∣ C_{e} (λ ∖ H) ∣ + e (w_{e} (λ) - 1) = ∣ C_{e} (λ) ∣ + e w_{e} (λ) - e,$ so $∣ λ ∣ = ∣ C_{e} (λ) ∣ + e w_{e} (λ)$ ; and appending the single step $H$ shows that every maximal sequence from $λ$ has exactly $w_{e} (λ)$ steps, because $H$ was an arbitrary possible first $e$ -hook removal and step 2.2 applies to every such first step.

4.1step 1.1step 2.1step 3.1discharge-induction: step 2.2∎

The base case of step 2.1 and the induction step of steps 2.2 and 3.1 establish the size formula and the step count for every partition of finite weight, and the counting statement is step 1.1. This is all that was asserted.

Depends on

Used by

Dependency tree · two levels

12 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

Stacey Law (lecturer), notes by Leonard Tomczak, Representation Theory of Symmetric Groups, Cambridge Part III Michaelmas 2022 lecture notes, complete 76-page PDF (standard reference, not scraped)