ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-04

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 complete singular local ring as a power-series quotient

Example

Let $k$ be a field and let $A = k ⟦ x, y ⟧ / (y^{2} - x^{3}) .$ Then $A$ is a complete equicharacteristic local ring presented as a quotient of a formal power-series ring; it is the standard cusp hypersurface.

Facts & Assumptions

Given: A field $k$ and the quotient ring $A = k ⟦ x, y ⟧ / (y^{2} - x^{3})$ .

[L1]

Complete equicharacteristic Noetherian local rings are quotients of formal power-series rings over their residue fields (A complete equicharacteristic Noetherian local ring is a power-series quotient).

Verification

technique · identify the explicit quotient map and its kernel

1.1

The canonical quotient map $k ⟦ X, Y ⟧ ↠ A, X \mapsto x, Y \mapsto y,$ has kernel containing the principal ideal $(Y^{2} - X^{3})$ by construction.

givenalgebra

2.1

Conversely, by definition $A$ is exactly the quotient by that relation, so the kernel is $(Y^{2} - X^{3})$ . Therefore $A ≅ k ⟦ X, Y ⟧ / (Y^{2} - X^{3}) .$ The maximal ideal is generated by the classes of $x$ and $y$ , and the relation has no linear term, so the ring is singular at that point.

step 1.1givenalgebra

3.1

This is an explicit instance of [L1]: the cusp local ring is a concrete complete local power-series quotient.

L1step 2.1∎

Depends on

A complete equicharacteristic Noetherian local ring is a power-series quotient

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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, 13th ed., Theorem 22.33 (standard reference, not scraped)