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 of (4,3,2,1) by two removal orders

Example

Let $e = 3$ and $λ = (4, 3, 2, 1) ⊢ 10$ , with $β$ -set $X = {7, 5, 3, 1}$ (Beta-sets, the shift, and the e-runner abacus of a partition). Two different orders of removing rim $3$ -hooks both terminate at the $3$ -core $(1)$ , in agreement with the order-independence theorem (The e-core is independent of the rim hook removal order): on the $3$ -abacus the beads $7, 5, 3, 1$ lie on runners $1, 2, 0, 1$ , and sliding beads up in any admissible order reaches the top-packed configuration ${4, 2, 1, 0}$ with $P = (1)$ ; two explicit manual removal orders of the corresponding rim $3$ -hooks, namely $(4, 3, 2, 1) \to (2, 2, 2, 1) \to (1, 1, 1, 1) \to (1)$ and $(4, 3, 2, 1) \to (4, 3) \to (2, 2) \to (1),$ reach the same partition, and no $3$ -hook remains at the end (Hooks are bead-gap pairs on the abacus, The e-quotient controls the hooks of e-divisible length). The size count $10 - 1 = 9 = 3 \cdot 3$ exhibits the weight $w_{3} ((4, 3, 2, 1)) = 3$ (The core-quotient size formula defines the weight).

No choice principle is used.

Facts & Assumptions

Given: $e = 3$ , the partition $λ = (4, 3, 2, 1)$ of $10$ with the $β$ -set $X = X_{λ} = {7, 5, 3, 1}$ , and $3$ -abacus positions $3 a + i$ on runner $i$ at row $a$ (Beta-sets, the shift, and the e-runner abacus of a partition).

[F1]

For a $β$ -set ${h_{1} > \dots > h_{m}}$ the partition is $P ({h_{1} > \dots > h_{m}}) = (h_{1} - (m - 1), \dots, h_{m} - 0)$ with trailing zeros deleted, and the elements of $X_{λ}$ are the first-column hook lengths of $λ$ (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 hook having length $b - g$ ; it has length divisible by $3$ exactly when $b \equiv g (m o d 3)$ , and removing it replaces $Y$ by $(Y ∖ {b}) \cup {g}$ , which is again a $β$ -set, of the partition obtained by deleting the corresponding rim hook of size $b - g$ (Hooks are bead-gap pairs on the abacus).

[F3]

A removable border strip of size $3$ is a removable $3$ -strip as in Removable border strips and their height, and the rim hook attached to the hook of a node has size the hook length by Hooks of a partition correspond bijectively to removable border strips; the $3$ -core $C_{3} (λ) = P (X^{(3)})$ is the top-packed set of the $3$ -abacus of a $β$ -set of $λ$ (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 $10 = ∣ λ ∣ = ∣ C_{3} (λ) ∣ + 3 w_{3} (λ)$ with $w_{3} (λ)$ the number of such removals in any maximal sequence (The e-core is independent of the rim hook removal order, The core-quotient size formula defines the weight).

Verification

technique · direct

1.1givenF1F3

Beads on the runners: $7 = 3 \cdot 2 + 1$ , $5 = 3 \cdot 1 + 2$ , $3 = 3 \cdot 1 + 0$ , $1 = 3 \cdot 0 + 1$ , so the row-label sets are $X_{0}^{(3)} = {1}$ (bead $3$ ), $X_{1}^{(3)} = {2, 0}$ (beads $7, 1$ ) and $X_{2}^{(3)} = {1}$ (bead $5$ ). Top-packing puts the single beads of runners $0$ and $2$ in row $0$ and the two beads of runner $1$ in rows $0, 1$ , so $X^{(3)} = {0} \cup {1, 4} \cup {2} = {4, 2, 1, 0}$ and, listing the four beads in decreasing order, $C_{3} (λ) = P (X^{(3)}) = (4 - 3, 2 - 2, 1 - 1, 0 - 0) = (1) .$

2.1givenF1F2F3step 1.1

The moves of a single bead one row up are exactly $7 \mapsto 4$ on runner $1$ , $5 \mapsto 2$ on runner $2$ and $3 \mapsto 0$ on runner $0$ , since $4, 2, 0 \notin X$ ; each target is a gap on the same runner as its bead, so by [F2] each move removes a rim hook of length $3$ . In particular $X^{(3)}$ is reached after exactly these three moves, in any order.

3.1F1F2F3step 1.1step 2.1construct

First removal order: move $7 \mapsto 4$ , then $5 \mapsto 2$ , then $3 \mapsto 0$ , giving the $β$ -sets ${7, 5, 3, 1} \to {5, 4, 3, 1} \to {4, 3, 2, 1} \to {4, 2, 1, 0}$ and, by [F1], the partitions $(4, 3, 2, 1) \to (2, 2, 2, 1) \to (1, 1, 1, 1) \to (1),$ each step of size $3$ by [F2] and [F3] and terminating at $C_{3} (λ) = (1)$ by step 1.1.

3.2F1F2F3step 1.1step 2.1construct

Second removal order: move $3 \mapsto 0$ , then $7 \mapsto 4$ , then $5 \mapsto 2$ , giving ${7, 5, 3, 1} \to {7, 5, 1, 0} \to {5, 4, 1, 0} \to {4, 2, 1, 0}$ and the partitions $(4, 3, 2, 1) \to (4, 3) \to (2, 2) \to (1),$ again three steps of size $3$ ending at $(1)$ ; both orders are maximal, since the terminal configuration ${4, 2, 1, 0}$ has no bead with a gap one row above it on its runner, so no rim $3$ -hook remains.

4.1F2F3F4step 1.1step 3.1step 3.2algebra∎

The size formula of [F4] reads $10 = ∣ C_{3} (λ) ∣ + 3 w_{3} (λ) = 1 + 3 \cdot 3$ , using step 1.1 and the three steps of either order; the partition $(1)$ has the single hook length $1$ , so indeed no hook of length $3$ survives, and the two orders agree on the terminal partition as asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Andrew Mathas, Hecke algebras and Schur algebras of the symmetric group, complete 79-page prepublication manuscript (1998; expanded AMS University Lecture Series 15 edition, 1999) (standard reference, not scraped)
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)