ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31

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 cusp local ring is not a DVR

Example

Let $A : = k [t^{2}, t^{3}] \subseteq k [t]$ , and let $m = (t^{2}, t^{3}) \subset A$ . Then the local ring $A_{m}$ is not a discrete valuation ring.

Facts & Assumptions

Given: A field $k$ , the cusp ring $A = k [t^{2}, t^{3}]$ , and the prime ideal $m = (t^{2}, t^{3})$ .

[F1]

Localisation at a prime ideal means inverting the complement of that prime (Localisation at a prime ideal: $R_{p} = (R ∖ p)^{- 1} R$ ).

[L1]

A nonfield domain is a DVR exactly when it is a one-dimensional Noetherian local integrally closed domain (Equivalent characterizations of a DVR).

Verification

technique · direct

1.1

The element $t \in k [t]$ is integral over $A_{m}$ because it satisfies the monic equation $T^{2} - t^{2} = 0$ with coefficient $t^{2} \in A \subseteq A_{m}$ .

F1givenalgebra

2.1

The element $t$ does not belong to $A_{m}$ . Indeed, if $t = a / s$ with $a \in A$ and $s \in A ∖ m$ , then $s t = a \in A$ . Since $s \notin m$ , its constant term is nonzero, so $s = c + t^{2} h (t)$ with $c \in k^{\times}$ . Then $s t = c t + t^{3} h (t)$ . Every element of $A = k [t^{2}, t^{3}]$ is a $k$ -linear combination of monomials $t^{n}$ with $n = 0$ or $n \geq 2$ , so no element of $A$ has a nonzero $t^{1}$ term. But $c t + t^{3} h (t)$ does, contradiction.

F1step 1.1algebra

3.1

Thus $A_{m}$ contains an element of its fraction field integral over it that does not lie in the ring. By [L1], $A_{m}$ is not a DVR.

L1step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

M. Mustata, Commutative Algebra, Proposition 8.7 (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (23.10) (standard reference, not scraped)