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.

Uniformisers and ideal arithmetic in a DVR

Example

Let $V$ be a discrete valuation ring. If $π$ and $π^{'}$ are uniformisers, then $π^{'} = u π$ for a unit $u \in V^{\times}$ . For all integers $m, n \geq 0$ , $(π^{m}) + (π^{n}) = (π^{\min {m, n}}), (π^{m}) \cap (π^{n}) = (π^{\max {m, n}}) .$

Facts & Assumptions

Given: A discrete valuation ring $V$ and two uniformisers $π, π^{'}$ .

[F1]

A uniformiser generates the maximal ideal of a DVR (Uniformising parameters).

[L1]

Every nonzero ideal of a DVR is a power of the maximal ideal (Ideals in a DVR are powers of the maximal ideal).

Verification

technique · direct

1.1

By [F1], both $π$ and $π^{'}$ generate the maximal ideal, so $(π) = (π^{'})$ . Hence $π^{'} \in (π)$ , say $π^{'} = u π$ , and similarly $π = v π^{'}$ . Multiplying gives $π = v u π$ , so $v u = 1$ in the domain $V$ and $u$ is a unit.

F1givenalgebra

2.1

The sum $(π^{m}) + (π^{n})$ is one of the two comparable ideals $(π^{m})$ and $(π^{n})$ , namely the larger one, so [L1] makes it $(π^{\min {m, n}})$ . Likewise the intersection is the smaller one, namely $(π^{\max {m, n}})$ .

L1step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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, Remark 8.9 (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, Discrete valuation rings after Example 20.1 (standard reference, not scraped)