ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

A disconnected skew Schur function factors

Statement

For $λ = (3, 1)$ and $μ = (1)$ , the two edge-disconnected components of $λ / μ$ give $s_{(3, 1) / (1)} = h_{2} h_{1} .$

Facts & Assumptions

Given: English Young-diagram coordinates, the stable rank projections and multiplication, complete homogeneous functions, skew-tableau conventions, and the skew Jacobi–Trudi and tableau formulas.

[F1]

In English coordinates, row $i$ of $[λ]$ contains $λ_{i}$ boxes, and trailing zeros pad partitions for row comparisons (Partitions, English diagrams, and conjugation).

[F2]

The stable ring is the graded direct sum of its degreewise inverse limits; multiplication is coordinatewise, and its rank projections set added variables to zero (The stable graded ring of symmetric functions).

[F3]

In $N$ variables, $h_{k}$ sums all monomials of total degree $k$ ; at rank zero $h_{k} = 0$ for $k > 0$ (Power sums $p_{k}$ and complete homogeneous symmetric polynomials $h_{k}$ ).

[F4]

The stable complete functions $h_{k}$ are compatible sequences obtained from the finite complete homogeneous polynomials, and $h_{ρ} = \prod_{i} h_{ρ_{i}}$ (Elementary and complete families freely generate the stable ring).

[F5]

Two skew boxes are side-adjacent when their coordinates differ by one in exactly one coordinate; edge-connected components use this adjacency (Skew diagrams and semistandard skew tableaux).

[F6]

A semistandard skew tableau is weakly increasing along rows and strictly increasing down columns (Skew diagrams and semistandard skew tableaux).

[F7]

At rank zero, $h_{k} = 0$ for $k > 0$ (Power sums $p_{k}$ and complete homogeneous symmetric polynomials $h_{k}$ ).

[F8]

For $μ \subseteq λ$ , every allowed padded size $r$ gives $s_{λ / μ} = \det (h_{λ_{i} - μ_{j} - i + j})$ and the sum of the weight monomials of semistandard skew tableaux; negative subscripts have value zero (Skew Jacobi–Trudi and tableau expansion).

Proof

technique · direct

1.1F1F5

Pad $μ = (1)$ to $(1, 0)$ . By [F1], the remaining cells of $λ / μ$ are exactly $(1, 2), (1, 3), (2, 1)$ . The first two share an edge; $(2, 1)$ shares no edge with either, since $(1, 1)$ was removed and $(1, 2)$ is only diagonally adjacent. Thus the components are the two-cell row and the single cell.

1.2F1F8algebra

The minimum allowed determinant size is $r = 2$ . Its matrix entries are $h_{3 - 1 - 1 + 1} = h_{2}$ , $h_{3 - 0 - 1 + 2} = h_{4}$ , $h_{1 - 1 - 2 + 1} = h_{- 1}$ , and $h_{1 - 0 - 2 + 2} = h_{1}$ , so [F8] gives $\det (\begin{array}{cc} h_{2} & h_{4} \\ 0 & h_{1} \end{array}) = h_{2} h_{1}$ . The off-diagonal $h_{4}$ term contributes zero because the lower-left entry is $h_{- 1} = 0$ .

1.3F2F3F4F5F6F8

A semistandard filling assigns entries $a \leq b$ to the top row and an arbitrary positive entry $c$ to the isolated lower cell; there is no row or column inequality connecting the components [F5, F6]. By [F3], its weight generating series in rank $N$ is $\sum_{1 \leq a \leq b \leq N} \sum_{1 \leq c \leq N} x_{a} x_{b} x_{c} = h_{2}^{(N)} h_{1}^{(N)}$ . The tableau formula [F8] and compatible stable products [F2, F4] therefore give $s_{(3, 1) / (1)} = h_{2} h_{1}$ in $Λ$ .

1.4F2F3F4

At rank $3$ , [F3] gives $h_{2}^{(3)} = x_{1}^{2} + x_{2}^{2} + x_{3}^{2} + x_{1} x_{2} + x_{1} x_{3} + x_{2} x_{3}$ and $h_{1}^{(3)} = x_{1} + x_{2} + x_{3}$ , hence $h_{2}^{(3)} h_{1}^{(3)} = x_{1}^{3} + x_{2}^{3} + x_{3}^{3} + 2 \sum_{i \neq j} x_{i}^{2} x_{j} + 3 x_{1} x_{2} x_{3}$ . Each cube occurs once, each $x_{i}^{2} x_{j}$ with $i \neq j$ occurs twice (from $x_{i}^{2} x_{j}$ and $x_{i} x_{j} x_{i}$ ), and the triple product occurs three times, once from each pair term of $h_{2}^{(3)}$ .

2.1F1F2F3F6F7F8algebra∎

The fixed skew shape has three boxes, so an empty-shape case does not arise. At rank zero both positive-degree complete functions vanish [F7] and no positive entry is available [F6]; at rank one [F3] gives $h_{2}^{(1)} h_{1}^{(1)} = x_{1}^{3}$ , matching the unique filling with $1$ in all three cells. Hence this example is nonzero, as the rank-three expansion also shows. The determinant uses its minimum size $r = 2$ [F8]; each finite-rank tableau set is finite and the compatible stable passage makes no choice. The example asserts no biconditional.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Chapter I §5 equations (5.4), (5.7), and (5.12), printed pp. 70–73 (standard reference, not scraped)