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

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.

In k[Y] subset k[X] with Y = X^2, distinct comparable primes do not share a contraction

Example

Let $k$ be an algebraically closed field, let $A : = k [Y]$ , and let $B : = k [X]$ with the inclusion $A ↪ B$ determined by $Y \mapsto X^{2}$ . Then any two distinct comparable prime ideals of $B$ have different contractions to $A$ .

Facts & Assumptions

Given: An algebraically closed field $k$ , the integral extension $k [Y] \subseteq k [X]$ with $Y = X^{2}$ , and the incomparability theorem (Comparable primes with the same contraction are equal under an integral map).

[L1]

Under an integral map, comparable primes with the same contraction are equal (Comparable primes with the same contraction are equal under an integral map).

Verification

technique · direct

1.1

Because $k$ is algebraically closed, the prime ideals of $k [X]$ are $(0)$ and the maximal ideals $(X - a)$ for $a \in k$ . The inclusion is integral because $X$ satisfies the monic equation $T^{2} - Y = 0$ over $k [Y]$ .

L1givenalgebra

2.1

The contractions are easy to compute: $(0) \cap k [Y] = (0)$ , while $(X - a) \cap k [Y] = (Y - a^{2})$ because a polynomial in $Y$ vanishes at $X = a$ exactly when it vanishes at $Y = a^{2}$ . Thus a proper inclusion of primes in $k [X]$ can only be $(0) ⊊ (X - a)$ , and its contractions are $(0) ⊊ (Y - a^{2})$ .

step 1.1givenalgebra

3.1

Hence every distinct comparable pair of primes in $k [X]$ has distinct contraction, exactly as [L1] predicts.

L1step 2.1∎

Depends on

Comparable primes with the same contraction are equal under an integral map

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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., Exercise (14.6) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, Corollary 7.4 (standard reference, not scraped)