ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Complete homogeneous symmetric polynomials and their recurrence in two variables

Example

In two variables $x, y$ ,

$h_{0} = 1, h_{1} = x + y, h_{2} = x^{2} + x y + y^{2}, h_{3} = x^{3} + x^{2} y + x y^{2} + y^{3} .$

For $k \geq 2$ they satisfy

$h_{k} = e_{1} h_{k - 1} - e_{2} h_{k - 2},$

and $e_{1} = h_{1}$ , $e_{2} = h_{1}^{2} - h_{2}$ .

Facts & Assumptions

Given: Two variables over a commutative ring.

[L1]

The identity $E (- t) H (t) = 1$ gives the coefficient recurrence among the $e_{i}$ and $h_{i}$ (The generating-series identity $E (- t) H (t) = 1$ ).

[L2]

The complete homogeneous polynomials $h_{1}, h_{2}$ freely generate the two-variable symmetric-polynomial ring (The complete homogeneous symmetric polynomials $h_{1}, \dots, h_{n}$ freely generate the symmetric-polynomial ring).

Verification

technique · direct

1.1

Listing all monomials of total degrees $0, 1, 2, 3$ gives the displayed values of $h_{0}, h_{1}, h_{2}, h_{3}$ .

givenalgebra

1.2

Here $E (- t) = 1 - e_{1} t + e_{2} t^{2}$ . Comparing the coefficient of $t^{k}$ in [L1] gives $h_{k} - e_{1} h_{k - 1} + e_{2} h_{k - 2} = 0$ for $k \geq 2$ .

L1algebra

2.1

At $k = 1$ the same identity gives $h_{1} = e_{1}$ , and at $k = 2$ it gives $h_{2} = e_{1} h_{1} - e_{2}$ , hence $e_{2} = h_{1}^{2} - h_{2}$ . This explicitly realizes the free-generation statement [L2].

step 1.2L1L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 10 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

D. Grinberg, An Introduction to Algebraic Combinatorics, Chapter 7, Section 7.1 (standard reference, not scraped)