ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-30

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 small Rabinowitsch identity written out completely

Example

Let $I = (x, y) \subseteq k [x, y]$ and let $f = x + y$ . Then the auxiliary ideal

I + (1 - u (x + y)) \subseteq k [x, y, u]

contains the explicit identity

1 = u x + u y + (1 - u (x + y)),

and clearing denominators after $u = 1 / (x + y)$ shows $x + y \in I$ .

Facts & Assumptions

Given: A field $k$ , the ideal $I = (x, y) \subseteq k [x, y]$ , and the polynomial $f = x + y$ .

[L1]

If $f$ vanishes on $V (I)$ , then the auxiliary ideal has empty zero locus (The Rabinowitsch auxiliary ideal has no common zero).

[L3]

Substituting the inverse of $f$ and clearing denominators yields a power of $f$ in $I$ (Substituting y = 1/f and clearing denominators yields a power of f in I).

Verification

technique · direct

1.1

The zero locus of $I = (x, y)$ is the single point $(0, 0)$ , and $f (0, 0) = 0$ . So the Rabinowitsch hypothesis holds. The displayed formula is already an explicit unit-ideal identity in the auxiliary ideal.

L1given

2.1

In the localization where $x + y$ is invertible, substitute $u = 1 / (x + y)$ into $1 = u x + u y + (1 - u (x + y))$ to get $1 = \frac{x}{x + y} + \frac{y}{x + y} .$ The zero-denominator case is excluded precisely because this localization inverts $x + y$ . Multiplying by $x + y$ yields $x + y = x + y \in I$ . This is the denominator-clearing step of [L3] with $N = 1$ .

L3step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

J. S. Milne, A Primer of Commutative Algebra, v4.03, Theorem 13.10 (standard reference, not scraped)