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.

Two minimal decompositions of (x2,xy) share radicals but not the embedded 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=(x)(x2,y).

The radical set is the same in both decompositions, but the embedded (x,y)-primary component changes.

Facts & Assumptions

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

[L1]

Over a Noetherian commutative ring, for a finitely generated module and a minimal primary decomposition whose component radicals are prime, the radical set depends only on the quotient (The radicals in a minimal primary decomposition are intrinsic).

[L2]

Assuming the Axiom of Choice, an isolated primary component with prime radical in the Noetherian finite-module setting is recovered by localization and contraction (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).

Verification

technique · direct
1.1

The inclusion (x2,xy)(x)(x,y)2 is immediate, and every element of the right side has the form xf with f(x,y), so (x2,xy)=(x)(x,y)2. Likewise (x2,xy)(x)(x2,y), and if xf(x2,y) then xf=x2a+yb for some a,b. The right-hand side lies in (x), so yb(x); thus b=xc and xf=x(xa+yc)(x2,xy). Hence (x2,xy)=(x)(x2,y).

givenalgebra
2.1

The field k is Noetherian because its only ideals are 0 and k, so [L3] makes R=k[x,y] Noetherian. The ideal (x) is prime because R/(x)k[y]. The quotients R/(x,y)2 and R/(x2,y)k[x]/(x2) are local rings with square-zero maximal ideals, so (x,y)2 and (x2,y) are (x,y)-primary. Both decompositions are irredundant: x(x) lies in neither (x,y)2 nor (x2,y), while y2(x,y)2(x) and y(x2,y)(x). Hence both displayed decompositions are minimal primary decompositions with prime radicals (x) and (x,y).

L3step 1.1algebra
3.1

Fact [L1] now predicts exactly the common radical set from step 2.1. The second component differs: one decomposition uses (x,y)2, the other uses (x2,y).

L1step 2.1
3.2

Localizing at the minimal prime (x) kills the (x,y)-primary component in either decomposition, so [L2] recovers the same isolated component (x) from both. The difference therefore lies only in the embedded component.

L2step 2.1
4.1

This is the standard warning that first uniqueness does not imply componentwise uniqueness of embedded pieces.

step 3.1step 3.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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