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.

The three-core and three-quotient of (6,5,2,1^3) by abacus

Example

Work with $e = 3$ and $λ = (6, 5, 2, 1^{3}) ⊢ 16$ , whose $β$ -set is $X_{λ} = {11, 9, 5, 3, 2, 1}$ (Beta-sets, the shift, and the e-runner abacus of a partition). On the $3$ -abacus the beads sit on runners $0, 1, 2$ at positions $9, 3$ on runner $0$ , $1$ on runner $1$ and $11, 5, 2$ on runner $2$ . Top-packing every runner gives the core beads $3, 0$ on runner $0$ , $1$ on runner $1$ and $8, 5, 2$ on runner $2$ , so $C_{3} (λ) = (3, 1)$ (The e-core, the e-quotient, and the e-weight); with the normalising condition $3 ∣ ∣ X ∣ = 6$ the runner row-label sets are $X_{0}^{(3)} = {3, 1}$ , $X_{1}^{(3)} = {0}$ and $X_{2}^{(3)} = {3, 1, 0}$ , giving the quotient $Q_{3} (λ) = ((2, 1), \emptyset, (1))$ . Four bead moves are required, and the size formula $16 = ∣ (3, 1) ∣ + 3 (∣ (2, 1) ∣ + ∣ \emptyset ∣ + ∣ (1) ∣) = 4 + 3 \cdot 4$ holds (The core-quotient size formula defines the weight); the same-runner bead-gap pairs realise the corresponding rim $3$ -hook removals (Hooks are bead-gap pairs on the abacus, The e-quotient controls the hooks of e-divisible length, The e-core is independent of the rim hook removal order).

No choice principle is used.

Facts & Assumptions

Given: $e = 3$ , the partition $λ = (6, 5, 2, 1^{3})$ of $16$ with $β$ -set $X = X_{λ} = {11, 9, 5, 3, 2, 1}$ , and the $3$ -abacus positions $3 a + i$ of runner $i$ and row $a$ (Beta-sets, the shift, and the e-runner abacus of a partition).

[F1]

A $β$ -set and its partition are related by $P ({h_{1} > \dots > h_{m}}) = (h_{1} - (m - 1), \dots, h_{m} - 0)$ with trailing zeros deleted; the elements of $X_{λ}$ are the first-column hook lengths $b_{i} (λ) = λ_{i} + ℓ (λ) - i$ (Beta-sets, the shift, and the e-runner abacus of a partition).

[F2]

The hooks of a partition with $β$ -set $Y$ correspond bijectively to the bead-gap pairs $(b, g)$ of $Y$ , i.e. $b \in Y$ , $g \notin Y$ , $0 \leq g < b$ , the corresponding hook having length $b - g$ ; the hook has length divisible by $3$ exactly when $b \equiv g (m o d 3)$ ; and removing it replaces $Y$ by $(Y ∖ {b}) \cup {g}$ (Hooks are bead-gap pairs on the abacus).

[F3]

On the $3$ -abacus the row-label set of runner $i$ is $Y_{i}^{(3)} = {a : 3 a + i \in Y}$ , the top-packed set is $Y^{(3)} = ⋃_{i = 0}^{2} {3 a + i : 0 \leq a \leq ∣ Y_{i}^{(3)} ∣ - 1}$ , the $3$ -core is $C_{3} (\cdot) = P (Y^{(3)})$ , and for a normalised $β$ -set with $3 ∣ ∣ Y ∣$ the $3$ -quotient components are $λ^{(i)} = P (Y_{i}^{(3)})$ with weight $w_{3} = ∣ Q_{3} ∣ = \sum_{i} ∣ λ^{(i)} ∣$ (The e-core, the e-quotient, and the e-weight).

[F4]

$C_{3} (λ)$ is the terminal partition of every maximal sequence of removals of removable border strips of size $3$ , and $∣ λ ∖ R ∣ = ∣ λ ∣ - 3$ for each such strip $R$ (The e-core is independent of the rim hook removal order).

[F5]

There is a bijection $f$ from the hooks of $λ$ of $3$ -divisible length onto the hooks of $Q_{3} (λ)$ with $∣ H ∣ = 3 ∣ f (H) ∣$ and $Q_{3} (λ ∖ H) = Q_{3} (λ) ∖ f (H)$ (The e-quotient controls the hooks of e-divisible length); and $16 = ∣ λ ∣ = ∣ C_{3} (λ) ∣ + 3 w_{3} (λ)$ with $w_{3} (λ)$ the number of such hooks (The core-quotient size formula defines the weight).

Verification

technique · direct

1.1givenF1F3

Beads on the runners: reading positions $3 a + i$ of $X = {11, 9, 5, 3, 2, 1}$ gives runner $0$ the positions $9 = 3 \cdot 3$ , $3 = 3 \cdot 1$ , runner $1$ the position $1 = 3 \cdot 0 + 1$ , and runner $2$ the positions $11 = 3 \cdot 3 + 2$ , $5 = 3 \cdot 1 + 2$ , $2 = 3 \cdot 0 + 2$ . Hence the row-label sets are $X_{0}^{(3)} = {3, 1}$ , $X_{1}^{(3)} = {0}$ , $X_{2}^{(3)} = {3, 1, 0}$ , of counts $2, 1, 3$ .

1.2givenF1F3

Top-packing moves the two beads of runner $0$ to rows $0, 1$ , the bead of runner $1$ to row $0$ , and the three beads of runner $2$ to rows $0, 1, 2$ , so $X^{(3)} = {0, 3} \cup {1} \cup {2, 5, 8} = {8, 5, 3, 2, 1, 0}$ and, by [F1] with the six beads listed in decreasing order, $C_{3} (λ) = P (X^{(3)}) = (8 - 5, 5 - 4, 3 - 3, 2 - 2, 1 - 1, 0 - 0) = (3, 1) .$

2.1givenF1F3step 1.1

The normalisation $3 ∣ ∣ X ∣ = 6$ holds, so the row-label sets of step 1.1 may be read as $1$ -abaci: $λ^{(0)} = P ({3, 1}) = (2, 1)$ , $λ^{(1)} = P ({0}) = \emptyset$ and $λ^{(2)} = P ({3, 1, 0}) = (1)$ , so $Q_{3} (λ) = ((2, 1), \emptyset, (1))$ and $w_{3} (λ) = 2 + 1 + 0 + 1 = 4$ .

2.2givenF1F2F4step 1.1step 1.2construct

Four upward bead moves lead from $X$ to $X^{(3)}$ : $11 \mapsto 8$ on runner $2$ (the target $8 \notin X$ ), then $9 \mapsto 6$ on runner $0$ ( $6 \notin X$ ), then $3 \mapsto 0$ on runner $0$ ( $0 \notin X$ ), then $6 \mapsto 3$ on runner $0$ (now $3 \notin X$ ); every move replaces a bead by a gap one row above it on its own runner, so by [F2] each is the removal of a rim hook of length $3$ . In terms of [F1] the intermediate partitions are $(6, 5, 2, 1^{3}) \to (4, 4, 2, 1^{3}) \to (3, 2, 2, 1^{3}) \to (3, 2, 2) \to (3, 1),$ each step of size $3$ by [F4], and the terminal partition is $C_{3} (λ) = (3, 1)$ as computed in step 1.2.

3.1F2F3F5step 1.1step 1.2step 2.1step 2.2algebra∎

The size formula of [F5] reads $16 = ∣ C_{3} (λ) ∣ + 3 w_{3} (λ) = 4 + 3 \cdot 4$ , using steps 1.2 and 2.1; the fourth move of step 2.2 is the last of the $w_{3} (λ) = 4$ removals of size $3$ exhibited there. The four hooks of $λ$ of $3$ -divisible length, read from the hook-length diagram (rows $11, 7, 5, 4, 3, 1$ ; $9, 5, 3, 2, 1$ ; $5, 1$ ; $3$ ; $2$ ; $1$ ), are $H_{1, 5}$ of length $3$ , $H_{2, 1}$ of length $9$ , $H_{2, 3}$ of length $3$ and $H_{4, 1}$ of length $3$ , and the bijection $f$ of [F5] sends them to the hooks $H_{1, 1} (λ^{(2)})$ , $H_{1, 1} (λ^{(0)})$ , $H_{1, 2} (λ^{(0)})$ , $H_{2, 1} (λ^{(0)})$ of sizes $1, 3, 1, 1$ of $(1)$ , $(2, 1)$ , matching $∣ H ∣ = 3 ∣ f (H) ∣$ in each case; all assertions of the Example are thereby checked.

Depends on

Used by

Nothing in the library uses this result yet.

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)