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.
Minimal primes over a proper ideal exist
Statement
Assume the Axiom of Choice.
Let be a commutative ring and let be a proper ideal. Then there exists a prime ideal of containing that is minimal with respect to inclusion among the prime ideals containing .
Facts & Assumptions
Given: A commutative ring , a proper ideal , and the Axiom of Choice.
If an ideal is disjoint from a multiplicative set, then some prime ideal contains it and stays disjoint from that set (A prime containing an ideal and avoiding a multiplicative set).
Assuming the Axiom of Choice, every nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).
Prime ideals are ordered by inclusion as ideals (Prime ideals and maximal ideals in a commutative ring).
Proof
The singleton set is multiplicative and is disjoint from because is proper. Applying [L1] gives at least one prime ideal containing . Let be the set of all prime ideals containing , ordered by reverse inclusion. Then .
Let be a chain. Put Then . To see that is prime, let and assume . Choose with and . Since is totally ordered by inclusion, either or . In the first case because ; in the second case . Either way one of the primes in the chain contains but neither factor, a contradiction. Thus , and it is an upper bound of in the reverse-inclusion order.
By [L2], the poset has a maximal element for reverse inclusion. Such an element is exactly a prime ideal minimal by ordinary inclusion among the primes containing .
Therefore every proper ideal lies under a minimal prime ideal.