ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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 ideal (x,y) in k[x,y]_(x,y) has two minimal generators

Example

Let $k$ be a field, let $R = k [x, y]_{(x, y)}$ with maximal ideal $m = (x, y) R$ , and let $M = m$ . Then $x$ and $y$ form a minimal generating set of $M$ , so $M$ needs exactly two generators.

Facts & Assumptions

Given: A field $k$ , the local ring $R = k [x, y]_{(x, y)}$ , its maximal ideal $m = (x, y) R$ , and the module $M = m$ .

[L1]

Because $k$ is a field, the ideal $(x, y) \subseteq k [x, y]$ is prime, so the localisation $k [x, y]_{(x, y)}$ is local with residue field $k$ (Localisation at a prime ideal: $R_{p} = (R ∖ p)^{- 1} R$ , $R_{p}$ is local with unique maximal ideal $p R_{p}$ , $R_{p} / p R_{p} ≅ Frac (R / p)$ is the residue field at $p$ ).

Verification

technique · direct

1.1

In $M / m M = m / m^{2}$ , the classes of $x$ and $y$ are nonzero and linearly independent over the residue field $k$ , because every element of $m^{2}$ has total degree at least $2$ .

L1algebra

1.2

Those same classes span $m / m^{2}$ , since every element of $m$ has image given by its linear part $a x + b y$ modulo $m^{2}$ .

L1algebra

2.1

By definition, $m = (x, y) R$ , so $x$ and $y$ generate $M$ . If a single element generated $M$ , then its image would generate $M / m M$ , contradicting steps 1.1 and 1.2. Hence ${x, y}$ is a minimal generating set of $m$ .

L1step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise 13.44 (standard reference, not scraped)