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.

Cauchy kernel through bidegree three

Example

Let $Ω_{\leq 3} : = \sum_{d = 0}^{3} Ω_{d, d}$ be the part of the Cauchy kernel in bidegrees $(d, d)$ with $0 \leq d \leq 3$ . Its complete–monomial and Schur expansions are computed below. Pairing the $x$ -factor with $s_{21} (x)$ gives $s_{21} (y)$ .

Facts & Assumptions

Given: The degreewise stable ring, the finite complete and monomial conventions, their stable bases, the Cauchy expansions, the Hall form, and Jacobi–Trudi.

[F1]

In the bidegree completion, $Ω (x, y) = \sum_{λ} h_{λ} (x) m_{λ} (y) = \sum_{λ} s_{λ} (x) s_{λ} (y)$ ; both sums are taken by diagonal bidegree (Power-sum, complete, and Schur expansions of the Cauchy kernel).

[F2]

Each $Λ^{d}$ is the inverse limit of the rank- $N$ homogeneous symmetric-polynomial parts, and multiplication is induced by rankwise polynomial multiplication (The stable graded ring of symmetric functions).

[F3]

In rank $N$ , $h_{k}$ is the sum of all monomials of total degree $k$ , with $h_{0} = 1$ (Power sums $p_{k}$ and complete homogeneous symmetric polynomials $h_{k}$ ).

[F4]

In rank $N$ , $m_{λ}$ is the sum of the distinct monomials whose exponent tuples are permutations of the padded tuple $λ$ (Monomial symmetric polynomials indexed by partitions).

[F5]

In rank $N$ , the $m_{λ}$ 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).

[F6]

The stable orbit sums $m_{λ}$ , for $λ ⊢ d$ , form a $Z$ -basis of $Λ^{d}$ and project to the finite orbit sums whenever $N \geq d$ (The monomial symmetric functions form the integral stable basis).

[F7]

The finite $h_{r}$ specialize compatibly to stable elements, and $h_{λ} = \prod_{i} h_{λ_{i}}$ denotes their stable product (Elementary and complete families freely generate the stable ring).

[F8]

The Hall form is graded and satisfies $⟨ h_{λ}, m_{μ} ⟩_{H} = δ_{λ μ}$ (The Hall inner product on symmetric functions).

[F9]

For $r \geq ℓ (λ)$ , $s_{λ} = \det (h_{λ_{i} - i + j})_{1 \leq i, j \leq r}$ , with $h_{0} = 1$ , negative subscripts zero, and the empty determinant equal to $1$ (Jacobi–Trudi and dual Jacobi–Trudi identities).

[F10]

The stable Schur functions form an orthonormal basis for the Hall form: $⟨ s_{λ}, s_{μ} ⟩_{H} = δ_{λ μ}$ (Schur functions form an orthonormal integral basis).

[F11]

The completed tensor product has diagonal bidegree kernel $Ω = \prod_{i, j} (1 - x_{i} y_{j})^{- 1}$ (Bidegree completion of two symmetric-function rings).

Verification

technique · direct

1.1F2F5F6

At rank $3$ , the projection $Λ^{d} \to A_{3}^{d}$ is an isomorphism for each $0 \leq d \leq 3$ : for $d > 0$ , every partition of $d$ has length at most $d \leq 3$ , and [F5] and [F6] identify the stable and finite monomial bases; for $d = 0$ , both components are $Z$ with basis $1$ . Thus finite rank- $3$ coefficient calculations determine the stable coefficients in all degrees used here.

2.1F3F4F7step 1.1algebra

At rank $3$ , grouping monomials by distinct exponent orbits and counting ordered products gives the complete-function identities below; $m_{2} m_{1} = m_{3} + m_{21}$ and $m_{11} m_{1} = m_{21} + 3 m_{111}$ , while types $(3), (2, 1), (1, 1, 1)$ occur in $h_{1}^{3}$ with multiplicities $1, 3, 3! = 6$ .

$h_{1} = m_{1}, h_{2} = m_{2} + m_{11}, h_{11} = h_{1}^{2} = m_{2} + 2 m_{11} .$

$h_{3} = m_{3} + m_{21} + m_{111}, h_{21} = h_{2} h_{1} = m_{3} + 2 m_{21} + 3 m_{111}, h_{111} = h_{1}^{3} = m_{3} + 3 m_{21} + 6 m_{111} .$

$m_{2} m_{1} = m_{3} + m_{21}, m_{11} m_{1} = m_{21} + 3 m_{111} .$

3.1F9step 2.1algebra

Jacobi–Trudi evaluates the Schur functions through degree three as shown; substituting step 2.1 gives the monomial expressions, including $s_{111} = h_{1}^{3} - 2 h_{2} h_{1} + h_{3}$ .

$s_{1} = h_{1}, s_{2} = h_{2}, s_{11} = h_{1}^{2} - h_{2}, s_{3} = h_{3}, s_{21} = h_{2} h_{1} - h_{3}, s_{111} = h_{1}^{3} - 2 h_{2} h_{1} + h_{3} .$

$s_{1} = m_{1}, s_{2} = m_{2} + m_{11}, s_{11} = m_{11}, s_{3} = m_{3} + m_{21} + m_{111}, s_{21} = m_{21} + 2 m_{111}, s_{111} = m_{111} .$

$s_{111} = (m_{3} + 3 m_{21} + 6 m_{111}) - 2 (m_{3} + 2 m_{21} + 3 m_{111}) + (m_{3} + m_{21} + m_{111}) = m_{111} .$

4.1F1step 1.1step 2.1step 3.1

The partitions of degrees $0, 1, 2, 3$ are respectively ${\emptyset}$ , ${(1)}$ , ${(2), (1, 1)}$ , and ${(3), (2, 1), (1, 1, 1)}$ , so [F1] gives these complete–monomial and Schur components of $Ω_{\leq 3}$ in bidegrees $(d, d)$ .

$Ω_{0, 0} = 1 \otimes 1, Ω_{1, 1} = h_{1} (x) \otimes m_{1} (y), Ω_{2, 2} = h_{2} (x) \otimes m_{2} (y) + h_{11} (x) \otimes m_{11} (y) .$

$Ω_{3, 3} = h_{3} (x) \otimes m_{3} (y) + h_{21} (x) \otimes m_{21} (y) + h_{111} (x) \otimes m_{111} (y) .$

$Ω_{0, 0} = 1 \otimes 1, Ω_{1, 1} = s_{1} (x) \otimes s_{1} (y), Ω_{2, 2} = s_{2} (x) \otimes s_{2} (y) + s_{11} (x) \otimes s_{11} (y) .$

$Ω_{3, 3} = s_{3} (x) \otimes s_{3} (y) + s_{21} (x) \otimes s_{21} (y) + s_{111} (x) \otimes s_{111} (y) .$

4.2F8step 2.1step 3.1algebra

Since $s_{21} = h_{21} - h_{3}$ , duality in [F8] gives $⟨ s_{21}, h_{3} ⟩_{H} = ⟨ h_{21} - h_{3}, m_{3} + m_{21} + m_{111} ⟩_{H} = 1 - 1 = 0$ .

4.3F8step 2.1step 3.1algebra

Similarly, $⟨ s_{21}, h_{21} ⟩_{H} = ⟨ h_{21} - h_{3}, m_{3} + 2 m_{21} + 3 m_{111} ⟩_{H} = 2 - 1 = 1$ .

4.4F8step 2.1step 3.1algebra

Also, $⟨ s_{21}, h_{111} ⟩_{H} = ⟨ h_{21} - h_{3}, m_{3} + 3 m_{21} + 6 m_{111} ⟩_{H} = 3 - 1 = 2$ .

5.1F1F8F10step 3.1step 4.1step 4.2step 4.3step 4.4

Gradedness removes degrees below three, so contracting the first factor in the complete–monomial expansion gives $m_{21} (y) + 2 m_{111} (y) = s_{21} (y)$ ; contraction of the Schur expansion gives the same result by [F10].

6.1F1F3F4F5F6F11step 2.1algebra∎

Degree $0$ gives $1 \otimes 1$ (and [F11] specializes to $1$ when either alphabet is zero); in degree $1$ , $h_{1} = m_{1} = s_{1}$ has coefficient one. Degree $3$ is the retained upper endpoint and rank $3$ is its threshold rank; repeated parts in $h_{11}$ and $h_{111}$ have the coefficients from step 2.1, while each $m_{λ}$ lists distinct monomials. All counts are finite, so no choice is used, and no equivalence is asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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 §4, equations (4.2)–(4.3), printed pp. 62–63 (standard reference, not scraped)
Jeremy L. Martin, Lecture Notes on Algebraic Combinatorics, §9.9, printed pp. 191–195 (standard reference, not scraped)