LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The leading multidegree of $e_{1}^{b_{1}} \dots e_{n}^{b_{n}}$ is $(b_{1} + \dots + b_{n}, b_{2} + \dots + b_{n}, \dots, b_{n})$ with coefficient one

Statement

Let $R$ be a commutative ring with $1 \neq 0$ . For $b_{1}, \dots, b_{n} \in N$ , the leading multidegree in $R [x_{1}, \dots, x_{n}]$ of $e_{1}^{b_{1}} \dots e_{n}^{b_{n}}$ is

$(b_{1} + \dots + b_{n}, b_{2} + \dots + b_{n}, \dots, b_{n}),$

and its leading coefficient is $1$ . Distinct tuples $(b_{1}, \dots, b_{n})$ give distinct leading multidegrees.

Facts & Assumptions

Given: A commutative ring $R$ with $1 \neq 0$ and natural numbers $b_{1}, \dots, b_{n}$ . The hypothesis $1 \neq 0$ is needed: over the zero ring every polynomial is $0$ , and [L2] gives a leading multidegree only for a nonzero polynomial.

[L1]

The elementary polynomial $e_{k}$ is the sum of all squarefree monomials of degree $k$ in the variables (The elementary symmetric polynomials $e_{0}, e_{1}, \dots, e_{n}$ ).

[L2]

Lexicographic leading multidegree is the greatest exponent tuple carrying a nonzero coefficient (Lexicographic order on exponent tuples and the multidegree of a nonzero polynomial).

Proof

technique · direct

1.1

The lexicographically leading monomial of $e_{k}$ is $x_{1} \dots x_{k}$ , and its coefficient is $1$ : at the first omitted variable, any other squarefree degree- $k$ monomial has exponent $0$ where this one has exponent $1$ .

L1L2

2.1

If $a >_{l e x} b$ first differs at coordinate $r$ , then for every $c$ the tuples $a + c$ and $b + c$ still first differ at $r$ , with the former coordinate larger. Thus, among the products formed from copies of the $e_{k}$ , the unique largest term is obtained by choosing the leading monomial from every factor. Its coefficient is $1$ .

step 1.1L2algebra

3.1

Applying step 2.1 to $e_{1}^{b_{1}} \dots e_{n}^{b_{n}}$ gives exponent $b_{k} + \dots + b_{n}$ on $x_{k}$ and coefficient $1$ .

step 1.1step 2.1algebra

4.1

The displayed cumulative sums determine $b_{n}$ and then successively $b_{n - 1}, \dots, b_{1}$ by adjacent subtraction, so the map from $b$ to the leading multidegree is injective.

step 3.1algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 8 results over 6 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

K. Conrad, Symmetric Polynomials, Section 2 (standard reference, not scraped)

The leading multidegree of e1b1⋯enbne1b1​​⋯enbn​​ is (b1+⋯+bn,b2+⋯+bn,…,bn)(b1​+⋯+bn​,b2​+⋯+bn​,…,bn​) with coefficient one