ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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 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, 462 = 3 \cdot 147 + 21, 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 N$ the symbol $k$ written inside $Z$ means $ι (k)$ , where $ι : N \to Z$ is the embedding of The naturals embed in the integers. Since $ι$ is injective and preserves addition, multiplication and order, each numerical identity and inequality below is the image of the corresponding one in $N$ , checked there by the ordinary decimal arithmetic of $N$ .

Facts & Assumptions

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

[L1]

$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 Z$ and $b > 0$ there is exactly one pair $(q, r)$ with $a = q b + r$ and $0 \leq r < b$ (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ).

[L3]

If $a = q b + r$ then $\gcd (a, b) = \gcd (b, r)$ (If $a = q b + 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 \geq 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) \geq 1$ unless $a = b = 0$ , The absolute value $∣ a ∣$ of an integer, Absolute value in $Z$ : $∣ a ∣ \geq 0$ ; $∣ a ∣ = 0$ exactly when $a = 0$ ; $∣ - a ∣ = ∣ a ∣$ ; $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ ; $- ∣ a ∣ \leq a \leq ∣ a ∣$ ; and $∣ a ∣ \leq c$ exactly when $- c \leq a \leq 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 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 - q v)$ , 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) \neq (0, 0)$ the equation $a x + b y = \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 ${a x + b y : x, y \in Z}$ ; in particular $a x + b y = \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 $a x + b y = \gcd (a, b)$ , so Bézout coefficients are computed and not merely shown to exist).

[L7]

$d ∣ a$ means $a = d q$ for some $q$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

Verification

technique · direct

1.1L1L2algebra

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

2.1step 1.1L3

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

2.2step 1.1L1algebra

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$ .

3.1step 2.1L1L4

$\gcd (21, 0) = ∣ 21 ∣ = 21$ , since $21 \geq 0$ . Hence $\gcd (1071, 462) = 21$ .

3.2step 2.2algebra

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

4.1step 1.1step 3.1L5

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.

4.2step 3.1step 2.2step 3.2L6

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

5.1step 3.1L7algebra∎

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

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 $a x + b y = \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

Dependency tree · 2 levels

Sources

Euclidean algorithm (Wikipedia)

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