Alphabeta Math
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.

✓ 1 result · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

The integers are a Euclidean domain with Euclidean function δ(b)=∣b∣

Example

The integral domain Z is a Euclidean domain. A Euclidean function is δ(b)=∣b∣, with the nonnegative integer ∣b∣ identified with its unique preimage in N.

Facts & Assumptions

Given: Integers a,b∈Z with b≠0.

[L1]

The integers form a commutative ring (The integers form a commutative ring).

[L2]

The canonical embedding N→Z is injective, preserves addition, multiplication and order, and has the nonnegative integers as its image; in particular it makes 1≠0 (The naturals embed in the integers).

[L3]

The product of two nonzero integers is nonzero (The integers have no zero divisors; multiplicative cancellation).

[L4]

A commutative ring with 1≠0 and no zero divisors is an integral domain (Zero divisor, and integral domain: a commutative ring with 1≠0 and no zero divisors).

[L7]

A Euclidean domain is an integral domain equipped with a natural-valued function satisfying the stated division alternative (Euclidean domain and Euclidean function).

Verification

technique · direct
1.1

By [L1]--[L4], Z is an integral domain.

L1L2L3L4
1.2

For each nonzero integer c, let δ(c)∈N be the unique natural number whose image in Z is ∣c∣; this is defined by [L2] and [L6].

L2L6
1.3

By [L5], choose q,r∈Z such that a=qb+r and 0≤r<∣b∣.

L5given
2.1

If r=0, this is the zero-remainder alternative in the Euclidean-domain definition. If r≠0, then ∣r∣=r because r≥0. If δ(b)≤δ(r), order preservation in [L2] would give ∣b∣≤∣r∣, contradicting step 1.3; hence δ(r)<δ(b).

step 1.2step 1.3L2L6algebra
3.1

Thus the integral domain in step 1.1 has the Euclidean function δ satisfying the required division property, so Z is a Euclidean domain.

step 1.1step 1.2step 2.1L7∎

Sources