Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28
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.

Localizing (x2,xy)=(x)(x,y)2 keeps only the matching component

Example

Assume the Axiom of Choice (The Axiom of Choice), and let k be a field.

In R=k[x,y],

(x2,xy)=(x)(x,y)2.

Localizing at (x) kills the (x,y)-primary component, while localizing at (x,y) preserves both components.

Facts & Assumptions

Given: The Axiom of Choice, a field k, the polynomial ring R=k[x,y], and the decomposition (x2,xy)=(x)(x,y)2.

[L1]

Assuming the Axiom of Choice, over a Noetherian commutative ring and in a finitely generated module, localizing a primary component away from its radical preserves it, while localizing at a multiplicative set meeting its radical turns it into the whole localized module (Localisation of a primary submodule either stays primary or becomes the whole module).

[L2]

Assuming the Axiom of Choice, an isolated primary component with prime radical in the Noetherian finite-module setting is recovered by localizing at its prime and contracting back (Isolated primary components are recovered by localization and contraction).

[L3]

A polynomial ring in finitely many variables over a Noetherian commutative ring is Noetherian (If R is Noetherian then R[x1,,xn] is Noetherian for every nN).

[L4]

A polynomial ring in finitely many variables over an integral domain is an integral domain (A polynomial ring in finitely many indeterminates over an integral domain is an integral domain).

[L5]

For a commutative ring and an ideal P, the quotient R/P is an integral domain if and only if P is prime (R/P is an integral domain if and only if P is a prime ideal).

[L6]

A proper ideal Q is p-primary when every zero divisor on R/Q acts nilpotently and AnnR(R/Q)=p (Primary submodules and primary ideals).

[L7]

A primary decomposition is minimal exactly when no component is redundant and the component radicals are pairwise distinct; an isolated component has a radical minimal among those radicals (Primary decompositions, minimality, and isolated components).

Verification

technique · direct
1.1

The field k is Noetherian because its only ideals are 0 and k, so [L3] makes R=k[x,y] Noetherian. As an R-module, R is finitely generated by 1. The inclusion (x2,xy)(x)(x,y)2 is immediate. Conversely, every element of (x)(x,y)2 has the form xf with f(x,y), hence lies in (x2,xy). So (x2,xy)=(x)(x,y)2.

L3givenalgebra
1.2

Since a field is an integral domain, [L4] makes k[y]R/(x) an integral domain, so [L5] makes (x) prime. If multiplication by a class aˉ on the domain R/(x) has nontrivial kernel, then aˉ=0; hence that multiplication is zero and therefore nilpotent. Also AnnR(R/(x))=(x), whose radical is (x). Thus [L6] shows that (x) is (x)-primary.

L4L5L6algebra
1.3

Put Q=(x,y)2. Every class in R/Q has the form c+αxˉ+βyˉ. If c0, this class is a unit, with inverse c1c2(αxˉ+βyˉ) because (xˉ,yˉ)2=0. Therefore every zero divisor lies in (xˉ,yˉ) and is square-zero, so every zero divisor on R/Q acts nilpotently. Moreover AnnR(R/Q)=Q and Q=(x,y): every element of (x,y) has square in Q, while fnQ forces the constant term of f to vanish. Finally, R/(x,y)k is a domain, so [L5] makes (x,y) prime. Thus [L6] shows that (x,y)2 is (x,y)-primary.

L5L6algebra
2.1

The two prime radicals (x) and (x,y) are distinct, with (x)(x,y). The decomposition from step 1.1 is irredundant: y2(x,y)2(x), so the component (x) is not redundant, while x(x)(x,y)2, so the component (x,y)2 is not redundant. By [L7], the displayed primary decomposition is minimal, and its (x)-primary component is isolated because (x) is the smaller of the two radicals.

L7step 1.1step 1.2step 1.3algebra
3.1

At the prime (x), the element y becomes a unit. Since y2(x,y)2, fact [L1] and steps 1.1–2.1 give ((x,y)2)(x)=R(x), while (x)(x) survives. Hence (x2,xy)(x)=(x)(x). Since step 2.1 proves that (x) is the isolated component of a minimal primary decomposition, fact [L2] says it contracts back to (x).

L1L2step 1.1step 1.2step 1.3step 2.1algebra
3.2

At the maximal ideal (x,y), neither prime radical meets the denominator set, so [L1] and steps 1.1–2.1 preserve both primary components. Thus the whole decomposition survives in R(x,y).

L1step 1.1step 1.2step 1.3step 2.1
4.1

This computation shows concretely how localization removes exactly the components whose radicals meet the denominator set.

step 3.1step 3.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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