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.

The Hilbert-Samuel multiplicity of a plane-curve singularity is read from its associated graded ring

Example

Let $R : = k [x, y]_{(x, y)} / (y^{2} - x^{3})$ with maximal ideal $m = (x, y) / (y^{2} - x^{3})$ . Then ${gr}_{m} (R) ≅ k [X, Y] / (Y^{2}),$ so the homogeneous piece of degree $n \geq 1$ has basis $X^{n}, X^{n - 1} Y$ and dimension $2$ . Consequently $χ_{m, R} (n) = 1 + \sum_{j = 1}^{n} 2 = 2 n + 1$ for $n \geq 1$ , and therefore $e_{m} (R) = 2.$

Facts & Assumptions

Given: A field $k$ , the cusp local ring $R$ above, and its maximal ideal $m$ .

[L1]

The associated graded ring packages the quotients $m^{n} / m^{n + 1}$ , and the Hilbert-Samuel function is their cumulative length (The associated graded ring and associated graded module of an ideal-adic filtration, The Hilbert-Samuel function and eventual Hilbert-Samuel polynomial of a finite local module).

[L2]

Hilbert-Samuel multiplicity is the leading coefficient scaled by the factorial (Hilbert-Samuel multiplicity as the factorial-scaled leading coefficient).

Verification

technique · direct

1.1L1givenalgebra

The initial form of $y^{2} - x^{3}$ has degree $2$ , namely $Y^{2}$ , so ${gr}_{m} (R) ≅ k [X, Y] / (Y^{2}) .$ Thus the degree- $0$ piece has dimension $1$ , and every degree- $n \geq 1$ piece has basis $X^{n}, X^{n - 1} Y$ .

1.2L1algebra

Therefore $ℓ_{R} (m^{0} / m) = 1$ and $ℓ_{R} (m^{n} / m^{n + 1}) = 2 (n \geq 1) .$ Summing these lengths as in [L1] gives $χ_{m, R} (n) = 2 n + 1$ for $n \geq 1$ .

1.3L2

The eventual polynomial is $2 n + 1$ , so its degree is $1$ and the leading coefficient is $2$ . Hence [L2] gives $e_{m} (R) = 2$ .

2.1algebra∎

Thus the multiplicity of the cusp is read directly from its tangent-cone graded ring.

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

Craig Huneke and Irena Swanson, Integral Closure, Chapter 1 (standard reference, not scraped)
Stacks Project, Section 10.59: Noetherian local rings (standard reference, not scraped)