ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-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.

$\gcd(1071, 462) = 21$ by the Euclidean algorithm, with the back-substitution giving $21 = 7 \cdot 462 - 3 \cdot 1071$

Example

The remainder descent of The Euclidean algorithm: for $a \in \mathbb{Z}$ and $b > 0$ the remainder descent from $(a,b)$ terminates, and the last nonzero remainder is $\gcd(a,b)$ from $(1071, 462)$ is

$1071 = 2 \cdot 462 + 147, \qquad 462 = 3 \cdot 147 + 21, \qquad 147 = 7 \cdot 21 + 0,$

so the second coordinates are $462,\; 147,\; 21,\; 0$ : the descent stops after three divisions, the last nonzero remainder is $21$ , and

$\gcd(1071, 462) \;=\; 21 .$

Reading the divisions backwards gives Bézout coefficients:

$21 \;=\; 462 - 3 \cdot 147 \;=\; 462 - 3(1071 - 2 \cdot 462) \;=\; 7 \cdot 462 - 3 \cdot 1071 ,$

that is, $1071 \cdot (-3) + 462 \cdot 7 = 21$ .

Numerals. For $k \in \mathbb{N}$ the symbol $k$ written inside $\mathbb{Z}$ means $\iota(k)$ , where $\iota : \mathbb{N} \to \mathbb{Z}$ is the embedding of The naturals embed in the integers. Since $\iota$ is injective and preserves addition, multiplication and order, each numerical identity and inequality below is the image of the corresponding one in $\mathbb{N}$ , checked there by the ordinary decimal arithmetic of $\mathbb{N}$ .

Facts & Assumptions

Given: The integers $1071$ , $462$ , $147$ , $21$ and $0$ , with numerals read as above through $\iota$ (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

[L1]

$\mathbb{Z}$ is a commutative ring, and its order is total, antisymmetric, transitive and compatible with addition (The integers form a commutative ring, Arithmetic on the integers, The integers form a totally ordered ring, Order on the integers).

[L2]

For $a \in \mathbb{Z}$ and $b > 0$ there is exactly one pair $(q,r)$ with $a = qb + r$ and $0 \le r < b$ (Division with remainder in $\mathbb{Z}$ : for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$ ).

[L3]

If $a = qb + r$ then $\gcd(a,b) = \gcd(b,r)$ (If $a = qb + r$ then $a, b$ and $b, r$ have exactly the same common divisors, so $\gcd(a,b) = \gcd(b,r)$ ).

[L4]

$\gcd(u,0) = |u|$ , and $|u| = u$ for $u \ge 0$ ( $\gcd$ is symmetric and unchanged by signs: $\gcd(a,b) = \gcd(b,a) = \gcd(|a|,|b|)$ ; moreover $\gcd(a,0) = |a|$ , $\gcd(a,1) = 1$ , $\gcd(a,a) = |a|$ , and $\gcd(a,b) \ge 1$ unless $a = b = 0$ , The absolute value $|a|$ of an integer, 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$ , Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L5]

The descent of The Euclidean algorithm: for $a \in \mathbb{Z}$ and $b > 0$ the remainder descent from $(a,b)$ terminates, and the last nonzero remainder is $\gcd(a,b)$ from $(a,b)$ with $b > 0$ sends $(u,v)$ with $v > 0$ to $(v, u - qv)$ , where $q$ is the quotient of $u$ by $v$ ; it terminates at the least index $N$ with vanishing second coordinate, and the last nonzero remainder equals $\gcd(a,b)$ .

[L6]

For $(a,b) \ne (0,0)$ the equation $ax + by = \gcd(a,b)$ has an integer solution (Bézout's identity: for integers $a, b$ not both zero, $\gcd(a,b)$ is the least positive element of $\{\, ax + by : x, y \in \mathbb{Z} \,\}$ ; in particular $ax + by = \gcd(a,b)$ has an integer solution), and the extended descent computes one (The extended Euclidean algorithm: the same descent produces integers $x, y$ with $ax + by = \gcd(a,b)$ , so Bézout coefficients are computed and not merely shown to exist).

[L7]

$d \mid a$ means $a = dq$ for some $q$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

Verification

technique · direct

1.1

The three divisions are correct and are the ones [L2] produces. First, $2 \cdot 462 = 924$ and $924 + 147 = 1071$ , with $0 \le 147 < 462$ . Second, $3 \cdot 147 = 441$ and $441 + 21 = 462$ , with $0 \le 21 < 147$ . Third, $7 \cdot 21 = 147$ and $147 + 0 = 147$ , with $0 \le 0 < 21$ . In each line the remainder satisfies the constraint of [L2], so by the uniqueness there it is the remainder.

L1L2algebra

2.1

Applying [L3] to the three identities in turn gives $\gcd(1071,462) = \gcd(462,147) = \gcd(147,21) = \gcd(21,0)$ .

step 1.1L3

2.2

Back-substitution. From the second division, $21 = 462 - 3 \cdot 147$ ; from the first, $147 = 1071 - 2 \cdot 462$ . Substituting, $21 = 462 - 3(1071 - 2 \cdot 462) = 462 + 6 \cdot 462 - 3 \cdot 1071 = 7 \cdot 462 - 3 \cdot 1071$ .

step 1.1L1algebra

3.1

$\gcd(21,0) = |21| = 21$ , since $21 \ge 0$ . Hence $\gcd(1071,462) = 21$ .

step 2.1L1L4

3.2

The result checks numerically: $7 \cdot 462 = 3234$ , $3 \cdot 1071 = 3213$ , and $3234 - 3213 = 21$ .

step 2.2algebra

4.1

In the language of [L5], the descent from $(1071,462)$ is $(1071,462) \mapsto (462,147) \mapsto (147,21) \mapsto (21,0)$ , so the second coordinates are $462, 147, 21, 0$ ; the least index with vanishing second coordinate is $N = 3$ , the last nonzero remainder is $21$ , and it equals $\gcd(1071,462)$ as [L5] asserts.

step 1.1step 3.1L5

4.2

So $1071 \cdot (-3) + 462 \cdot 7 = 21 = \gcd(1071,462)$ , an explicit instance of [L6] with $(x,y) = (-3, 7)$ .

step 3.1step 2.2step 3.2L6

5.1

Finally $21 \mid 1071$ and $21 \mid 462$ directly: $21 \cdot 51 = 1071$ and $21 \cdot 22 = 462$ , so the value found is indeed a common divisor, as it must be.

step 3.1L7algebra∎

Remarks

Three divisions, and the count is exact for this pair only. Nothing here, and nothing on the companion page, proves a bound on the number of divisions in terms of the size of the inputs.
The back-substitution is not a second algorithm. It is the same descent read in reverse, and The extended Euclidean algorithm: the same descent produces integers $x, y$ with $ax + by = \gcd(a,b)$ , so Bézout coefficients are computed and not merely shown to exist performs it forwards, carrying the coefficient pairs alongside the remainders instead of recovering them afterwards.
The coefficients are not unique: $1071 \cdot 19 + 462 \cdot (-44) = 21$ as well, and Bézout coefficients are not unique: $1071 \cdot (-3) + 462 \cdot 7 = 21$ and $1071 \cdot 19 + 462 \cdot (-44) = 21$ , and for nonzero $a, b$ every solution has the form $(x_0 + t b/d,\; y_0 - t a/d)$ describes the whole family.

Depends on

Used by

Bézout coefficients are not unique: 1071 · (-3) + 462 · 7 = 21 and 1071 · 19 + 462 · (-44) = 21, and for nonzero a, b every solution has the form (x₀ + t b/d, y₀ - t a/d) Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 21 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

Euclidean algorithm (Wikipedia) (standard reference, not scraped)

gcd⁡(1071,462)=21\gcd(1071, 462) = 21gcd(1071,462)=21 by the Euclidean algorithm, with the back-substitution giving 21=7⋅462−3⋅107121 = 7 \cdot 462 - 3 \cdot 107121=7⋅462−3⋅1071