ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated

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 padded family $V ((2, 1))$ begins at rank five, with weight three and stability degree two

Example

Let $λ = (2, 1)$ , so $m : = ∣ λ ∣ = 3$ and $λ_{1} = 2$ , and let $λ [n]$ be the first-row padding (First-row padding of a partition). Then $λ [n] = (n - 3, 2, 1)$ , and this is a partition exactly for

$n \geq 5 = ∣ λ ∣ + λ_{1} :$

for $n = 3$ the sequence $(0, 2, 1)$ is not weakly decreasing, for $n = 4$ the sequence $(1, 2, 1)$ still is not, and for $n \geq 5$ the first entry $n - 3$ is at least $λ_{1} = 2$ , so the sequence is a partition of $n$ . The padded family therefore begins at rank five, two ranks later than $∣ λ ∣ = 3$ .

Accordingly, for a field $k$ of characteristic $0$ , the FI-module $V ((2, 1))$ of Each padded irreducible family is realised by a finitely generated FI-module has values

$V ((2, 1))_{n} ≅ V_{(n - 3, 2, 1)} (n \geq 5), V ((2, 1))_{n} = 0 (n < 5),$

is generated in degree exactly $5$ , and has $weight (V ((2, 1))) = 3$ and $inj-deg (V ((2, 1))) = 0$ , $surj-deg (V ((2, 1))) = stab-deg (V ((2, 1))) = 2$ (Weight of an FI-module over a field of characteristic zero, Injectivity, surjectivity and stability degree). For instance $V ((2, 1))_{5} ≅ V_{(2, 2, 1)}$ , $V ((2, 1))_{6} ≅ V_{(3, 2, 1)}$ and so on: the first row grows while the second row stays at $2$ . No choice principle is used.

Facts & Assumptions

Given: A field $k$ of characteristic $0$ ; the partition $λ = (2, 1)$ with $m = ∣ λ ∣ = 3$ and $λ_{1} = 2$ , the integers $d = m + λ_{1} = 5$ , and the first-row padding $λ [n]$ (First-row padding of a partition).

[F1]

$α [n] = (n - ∣ α ∣, α_{1}, α_{2}, \dots)$ is defined and a partition of $n$ exactly for $n \geq ∣ α ∣ + α_{1}$ ; for smaller nonnegative $n \geq ∣ α ∣$ the displayed sequence fails to be weakly decreasing (First-row padding of a partition).

[F2]

For a field $k$ of characteristic $0$ and a partition $α$ with $∣ α ∣ = m^{'}$ , $d^{'} = m^{'} + α_{1}$ , there is a sub-FI-module $V (α) \subseteq M (α)$ with $V (α)_{n} ≅ V_{α [n]}$ for $n \geq d^{'}$ and $V (α)_{n} = 0$ for $n < d^{'}$ ; its generation degree is exactly $d^{'}$ , and $weight (V (α)) = m^{'}$ , $inj-deg (V (α)) = 0$ , $surj-deg (V (α)) = stab-deg (V (α)) = α_{1}$ (Each padded irreducible family is realised by a finitely generated FI-module).

[F3]

For $η ⊢ n$ , $V_{η}$ is the irreducible $k S_{n}$ -module with label $η$ ; in particular $V_{λ [n]}$ is the irreducible labelled by the padded partition, and $∣ η ∣ - η_{1}$ (with $η_{1} = 0$ when $η = \emptyset$ ) is the size of the padding tail, hence the weight label of that irreducible (Specht modules classify the irreducibles over every field of characteristic zero, Weight of an FI-module over a field of characteristic zero).

[F4]

The injectivity, surjectivity and stability degrees of an FI-module are those of Injectivity, surjectivity and stability degree, with $stab-deg = \max (inj-deg, surj-deg)$ .

Verification

technique · direct

1.1F1given

Substituting $λ = (2, 1)$ gives $λ [n] = (n - 3, 2, 1)$ : for $n < 3$ the first entry is negative, for $n = 3$ it is $0 < 2$ and for $n = 4$ it is $1 < 2$ , so in these cases the sequence is not a partition; for $n \geq 5$ the first entry is at least $2$ , the entries are nonnegative and weakly decreasing and their sum is $(n - 3) + 2 + 1 = n$ . Hence $λ [n]$ is a partition exactly for $n \geq 5 = ∣ λ ∣ + λ_{1}$ .

2.1F2F3F4step 1.1

Apply [F2] with $α = λ = (2, 1)$ , so $m^{'} = 3$ and $d^{'} = 5$ : there is a sub-FI-module $V ((2, 1))$ of $M ((2, 1))$ with $V ((2, 1))_{n} ≅ V_{λ [n]} = V_{(n - 3, 2, 1)}$ for $n \geq 5$ and $V ((2, 1))_{n} = 0$ for $n < 5$ , of generation degree exactly $5$ , weight $3$ , injectivity degree $0$ and surjectivity degree $2$ , so that its stability degree is $2$ .

3.1F2F3step 1.1step 2.1∎

Steps 1.1 and 2.1 show that the padded family $V ((2, 1))$ begins at rank five, not at $∣ λ ∣ = 3$ , is generated in degree $5$ , and has weight $3$ and stability degree $2$ ; the second row of each constituent diagram $λ [n] = (n - 3, 2, 1)$ remains $2$ while the first row grows. No choice principle is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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

Thomas Church, Jordan S. Ellenberg and Benson Farb, “FI-modules and stability for representations of symmetric groups”, arXiv:1204.4533v4 (2014); published in Duke Math. J. 164 (2015) 1833–1910 (standard reference, not scraped)
I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Oxford Mathematical Monographs, 1995 (author-hosted full text) (standard reference, not scraped)

The padded family V((2,1))V((2,1)) begins at rank five, with weight three and stability degree two