CounterexampleConstruction: 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.

Power sums fail to span integrally in degree two

Statement

In degree two, the integral stable symmetric function $h_{2} = \frac{p_{(1, 1)} + p_{(2)}}{2}$ cannot be expressed as a $Z$ -linear combination of $p_{(1, 1)}$ and $p_{(2)}$ . Thus the power-sum family does not span $Λ^{2}$ over $Z$ .

Facts & Assumptions

Given: The stable graded ring, the finite power-sum and complete-homogeneous conventions, the finite monomial orbit sums, the stable monomial and complete bases, and the rational power-sum basis.

[F1]

Each $Λ^{d}$ is the inverse limit of its finite-rank homogeneous symmetric-polynomial pieces, and the rank- $N$ projections are compatible (The stable graded ring of symmetric functions).

[F2]

In rank $N$ , $p_{r} = \sum_{i = 1}^{N} x_{i}^{r}$ for $r \geq 1$ , and $h_{k}$ is the sum of all monomials of total degree $k$ (Power sums $p_{k}$ and complete homogeneous symmetric polynomials $h_{k}$ ).

[F3]

At rank $N$ , $m_{λ}$ is the sum of the distinct monomials in the variable-permutation orbit of the padded partition $λ$ (Monomial symmetric polynomials indexed by partitions).

[F4]

The stable $h_{r}$ are the compatible sequences obtained from the finite $h_{r}$ by setting added variables to zero (Elementary and complete families freely generate the stable ring).

[F5]

The stable functions $m_{(2)}$ and $m_{(1, 1)}$ form a $Z$ -basis of $Λ^{2}$ , and projection to rank $N = 2$ identifies this basis with the finite orbit sums (The monomial symmetric functions form the integral stable basis).

[F6]

The stable power-sum products $p_{λ}$ for $λ ⊢ 2$ form a $Q$ -basis of $Λ_{Q}^{2}$ (Power sums form a rational but not integral stable basis).

[F7]

In rank $N$ , the monomial orbit sums indexed by partitions of length at most $N$ form a $Z$ -basis of the symmetric polynomials (Monomial symmetric polynomials form an $R$ -basis of the symmetric-polynomial ring).

Proof

technique · direct

1.1F1F2F3F4F5F7algebra

At rank two, [F2] and [F3] give $m_{(2)} = x_{1}^{2} + x_{2}^{2}$ , $m_{(1, 1)} = x_{1} x_{2}$ , $h_{2} = m_{(2)} + m_{(1, 1)}$ , $p_{1}^{2} = m_{(2)} + 2 m_{(1, 1)}$ , and $p_{2} = m_{(2)}$ . By [F7], $m_{(2)}$ and $m_{(1, 1)}$ are a basis in rank two; by [F5] and the stable-ring projection in [F1], the rank-two projection $Λ^{2} \to A_{2}^{2}$ carries the stable basis to that finite basis and is an isomorphism. The stable $h_{2}$ projects to its finite polynomial by [F2] and [F4], and the finite power sums form compatible stable sequences by [F1] and [F2]. Thus the same three equations hold in $Λ^{2}$ . At rank one the three finite functions $h_{2}, p_{1}^{2}, p_{2}$ all equal $x_{1}^{2}$ , while rank zero has no degree-two monomials; rank two is the first rank that distinguishes the two monomial orbits.

2.1F5F6step 1.1algebra∎

Since $p_{(1, 1)} = p_{1}^{2}$ , step 1.1 yields $h_{2} = \frac{1}{2} (p_{(1, 1)} + p_{(2)})$ . By [F6], $p_{(1, 1)}$ and $p_{(2)}$ are a $Q$ -basis, so this is the unique rational coordinate vector of $h_{2}$ . If $h_{2} = a p_{(1, 1)} + b p_{(2)}$ for integers $a, b$ , including zero values, uniqueness forces $a = b = \frac{1}{2}$ , impossible. Equivalently, comparison in the integral basis of [F5] forces the $m_{(1, 1)}$ coefficient to satisfy $2 a = 1$ . Thus $h_{2}$ is a witness to failure of integral spanning.

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

I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Chapter I §2, equations (2.10)–(2.14′), printed pp. 23–25 (standard reference, not scraped)
Jeremy L. Martin, Lecture Notes on Algebraic Combinatorics, §9.6, printed pp. 181–183 (standard reference, not scraped)