ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-09-24 (gpt-6-sol)

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 DVR has Hilbert-Samuel polynomial $n + 1$ and multiplicity one

Example

Let $(V, (π))$ be a discrete valuation ring. Then $χ_{(π), V} (n) = ℓ_{V} (V / (π^{n + 1})) = n + 1$ for every $n \geq 0$ . Hence the Hilbert-Samuel polynomial is exactly $n + 1$ , and the Hilbert-Samuel multiplicity is $e_{(π)} (V) = 1.$

Facts & Assumptions

Given: A discrete valuation ring $V$ with maximal ideal $(π)$ .

[L1]

The quotient $V / (π^{n + 1})$ has length $n + 1$ for every $n \geq 0$ (Length and valuation in a DVR).

[L2]

When the Hilbert-Samuel function is explicitly polynomial, multiplicity is its factorial-scaled leading coefficient (Hilbert-Samuel multiplicity as the factorial-scaled leading coefficient).

Verification

technique · direct

1.1L1given

By [L1], the Hilbert-Samuel function is $χ_{(π), V} (n) = ℓ_{V} (V / (π^{n + 1})) = n + 1$ for every $n \geq 0$ .

1.2L2

Therefore the eventual polynomial is already exactly $P (n) = n + 1$ . Its degree is $1$ and its leading coefficient is $1$ , so [L2] gives $e_{(π)} (V) = 1! \cdot 1 = 1.$

2.1algebra∎

This computes both the Hilbert-Samuel polynomial and the multiplicity of a DVR.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, §§21 and 23 (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, discrete valuation rings (standard reference, not scraped)

A DVR has Hilbert-Samuel polynomial n+1n+1 and multiplicity one