CorollaryStatement: AI-adaptedProof: 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.

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

Statement

Let $a \in Z$ and $b > 0$ , and let $R (k) = (a_{k}, b_{k})$ and $N$ be the remainder descent and its terminating index from 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)$ . Define $Ψ : Z^{6} \to Z^{6}$ by

$Ψ (A, B, x, y, u, v) = {\begin{cases} (B, A - q B, u, v, x - q u, y - q v) & if B > 0, \\ (A, B, x, y, u, v) & if B \leq 0, \end{cases}$

where in the first clause $q$ is the unique quotient of $A$ by $B$ given by 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$ . Let

$S : N \to Z^{6}, S (0) = (a, b, 1, 0, 0, 1), S (σ (k)) = Ψ (S (k))$

be the function supplied by the recursion theorem (The recursion theorem), and write $S (k) = (A_{k}, B_{k}, x_{k}, y_{k}, u_{k}, v_{k})$ . Then for every $k \in N$

$(A_{k}, B_{k}) = (a_{k}, b_{k}), A_{k} = a x_{k} + b y_{k}, B_{k} = a u_{k} + b v_{k} .$

In particular, at the terminating index $N$ ,

$a x_{N} + b y_{N} = A_{N} = a_{N} = \gcd (a, b),$

so the descent that computes $\gcd (a, b)$ computes a pair of Bézout coefficients alongside it.

Facts & Assumptions

Given: $a \in Z$ , $b > 0$ , the descent $R (k) = (a_{k}, b_{k})$ and terminating index $N$ 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)$ , and the map $Ψ$ and sequence $S (k) = (A_{k}, B_{k}, x_{k}, y_{k}, u_{k}, v_{k})$ described above.

[L1]

$Z$ is a commutative ring: addition and multiplication are associative and commutative, $x + 0 = x$ , $x \cdot 1 = x$ , $x \cdot 0 = 0$ , multiplication distributes over addition, and every $x$ has an additive inverse; we write $u - v$ for $u + (- v)$ (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

For $A^{'} \in Z$ and $B^{'} > 0$ there is exactly one pair $(q, r)$ of integers 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]

For a set $X$ , an $α \in X$ and $f : X \to X$ there is exactly one $g : N \to X$ with $g (0) = α$ and $g (σ (k)) = f (g (k))$ (The recursion theorem, The natural numbers $N$ (von Neumann)).

[L4]

Induction on $N$ (The principle of mathematical induction).

[L5]

The descent satisfies $R (0) = (a, b)$ ; $b_{k} \geq 0$ for every $k$ ; $R (σ (k)) = (b_{k}, a_{k} - q b_{k})$ with $q$ the quotient of $a_{k}$ by $b_{k}$ when $b_{k} > 0$ , and $R (σ (k)) = R (k)$ when $b_{k} = 0$ ; $N$ is the least index with $b_{N} = 0$ ; and $a_{N} = \gcd (a, b)$ (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)$ , Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

[L6]

The order on $Z$ is total and antisymmetric; $x < y$ means $x \leq y$ together with $x \neq y$ (The integers form a totally ordered ring, Order on the integers).

Proof

technique · induction

1.1

$Ψ$ is a well-defined function: for $B > 0$ the quotient $q$ of $A$ by $B$ is unique by [L2], so the first clause depends only on the argument; the second clause is the identity; and the two conditions $B > 0$ and $B \leq 0$ are exhaustive and exclusive by totality. So [L3] applies with $X = Z^{6}$ and produces $S$ .

L1L2L3L6construct

1.2

Base case, $k = 0$ : $(A_{0}, B_{0}) = (a, b) = (a_{0}, b_{0})$ ; and $A_{0} = a = a \cdot 1 + b \cdot 0 = a x_{0} + b y_{0}$ , $B_{0} = b = a \cdot 0 + b \cdot 1 = a u_{0} + b v_{0}$ .

basegivenL1L5

1.3

Induction hypothesis: fix $k$ and assume $(A_{k}, B_{k}) = (a_{k}, b_{k})$ , $A_{k} = a x_{k} + b y_{k}$ and $B_{k} = a u_{k} + b v_{k}$ .

2.1

Inductive step, case $b_{k} > 0$ . Then $B_{k} = b_{k} > 0$ , so both recursions take their first clause with the same divisor and the same dividend, hence with the same quotient $q$ by [L2]. Therefore $(A_{σ (k)}, B_{σ (k)}) = (B_{k}, A_{k} - q B_{k}) = (b_{k}, a_{k} - q b_{k}) = (a_{σ (k)}, b_{σ (k)})$ .

step 1.3L2L5

2.2

Inductive step, case $b_{k} = 0$ . Then $B_{k} = b_{k} = 0$ , so $B_{k} \leq 0$ and $S (σ (k)) = S (k)$ , while $R (σ (k)) = R (k)$ ; all three equalities are inherited unchanged. Since $b_{k} \geq 0$ , the two cases are exhaustive.

step 1.3L5L6

3.1

Back in the case $b_{k} > 0$ of step 2.1, the coefficients transport: $A_{σ (k)} = B_{k} = a u_{k} + b v_{k} = a x_{σ (k)} + b y_{σ (k)}$ , since $(x_{σ (k)}, y_{σ (k)}) = (u_{k}, v_{k})$ ; and $B_{σ (k)} = A_{k} - q B_{k} = (a x_{k} + b y_{k}) - q (a u_{k} + b v_{k}) = a (x_{k} - q u_{k}) + b (y_{k} - q v_{k}) = a u_{σ (k)} + b v_{σ (k)}$ by distributivity.

step 1.3step 2.1L1

4.1

By induction the three equalities hold for every $k \in N$ .

step 1.2step 2.1step 3.1step 2.2L4

5.1

At the terminating index $N$ this reads $a x_{N} + b y_{N} = A_{N} = a_{N} = \gcd (a, b)$ , so $(x_{N}, y_{N})$ is a pair of Bézout coefficients for $a$ and $b$ , obtained from the descent itself.

step 4.1L5discharge-induction∎

Remarks

What "computed" means here. The coefficients are produced by a recursion over $N$ whose every step is an application of the division algorithm and four ring operations; nothing in the argument appeals to the existence of a least element of a set. That is the difference from 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, where the coefficients come from a well-ordering argument and the proof gives no way to find them.
The Bézout pair produced is not the only one. The companion page records the full family of solutions and a second pair for the same equation (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)$ ↗).
Only the first four coordinates of $S$ are needed for the conclusion; the last two are carried because the recursion for $(x, y)$ reads off the previous values of $(u, v)$ , which is what makes the whole thing a single application of the recursion theorem instead of a mutual recursion.

Depends on

Used by

Dependency tree · two levels

43 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

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

The extended Euclidean algorithm: the same descent produces integers x,yx,y with ax+by=gcd⁡(a,b)ax+by=gcd(a,b), so Bézout coefficients are computed and not merely shown to exist