ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03

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.

The integers are a Euclidean domain with Euclidean function $\delta(b)=|b|$

Example

The integral domain $\mathbb Z$ is a Euclidean domain. A Euclidean function is $\delta(b)=|b|$ , with the nonnegative integer $|b|$ identified with its unique preimage in $\mathbb N$ .

Facts & Assumptions

Given: Integers $a,b\in\mathbb Z$ with $b\ne0$ .

[L1]

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

[L2]

The canonical embedding $\mathbb N\to\mathbb Z$ is injective, preserves addition, multiplication and order, and has the nonnegative integers as its image; in particular it makes $1\ne0$ (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\ne0$ and no zero divisors is an integral domain (Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors).

[L5]

For $b\ne0$ , there are $q,r\in\mathbb Z$ with $a=qb+r$ and $0\le r<|b|$ (Division with remainder for any nonzero divisor: for $a \in \mathbb{Z}$ and $b \ne 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < |b|$ ).

[L6]

Integer absolute values are nonnegative, vanish exactly at zero, and satisfy $|r|=r$ for $r\ge0$ (Absolute value in $\mathbb{Z}$ : $|a| \ge 0$ ; $|a| = 0$ exactly when $a = 0$ ; $|-a| = |a|$ ; $|ab| = |a|\,|b|$ ; $-|a| \le a \le |a|$ ; and $|a| \le c$ exactly when $-c \le a \le c$ , The absolute value $|a|$ of an integer).

[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], $\mathbb Z$ is an integral domain.

L1L2L3L4

1.2

For each nonzero integer $c$ , let $\delta(c)\in\mathbb N$ be the unique natural number whose image in $\mathbb Z$ is $|c|$ ; this is defined by [L2] and [L6].

L2L6

1.3

By [L5], choose $q,r\in\mathbb Z$ such that $a=qb+r$ and $0\le r<|b|$ .

L5given

2.1

If $r=0$ , this is the zero-remainder alternative in the Euclidean-domain definition. If $r\ne0$ , then $|r|=r$ because $r\ge0$ . If $\delta(b)\le\delta(r)$ , order preservation in [L2] would give $|b|\le|r|$ , contradicting step 1.3; hence $\delta(r)<\delta(b)$ .

step 1.2step 1.3L2L6algebra

3.1

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

step 1.1step 1.2step 2.1L7∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 54 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Romyar Sharifi, Abstract Algebra (standard reference, not scraped)

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