Constructive Euclidean execution and complexity — Exact Proof Explorer

A nonzero Euclidean divisor constructively yields an exact quotient and strictly smaller remainder.

Two exact bounded Euclidean divisions of the same inputs have identical quotients and remainders.

Every nonterminal Euclidean remainder constructively admits the next genuine bounded division.

Constructive strict natural order remains strict after adding the same right summand.

After one strict Euclidean decrease, the quotient of the next division cannot be zero.

Any two consecutive genuine bounded Euclidean divisions strictly halve the starting divisor: twice the second remainder is smaller.

An already witnessed complete beta-coded history remains within the successor of its original linear step budget.

Bounded natural induction constructs an authentic complete Euclidean beta-history using at most B divisions whenever the divisor is at most B.

Every natural input pair admits an actual terminating Euclidean beta-trace whose exact division count is at most its initial divisor.

The zero-divisor boundary has an actual zero-step beta-history and returns the dividend as its checked relational gcd.

Every expanded Euclidean execution independently certifies its output against the original relational gcd specification.

Every expanded Euclidean execution contains an actual complete beta-coded history, not an abstract oracle or opaque trace predicate.

All natural input pairs admit a fully expanded, beta-coded terminating Euclidean execution with a certified relational gcd output.

For every nonzero initial divisor, an actual certified Euclidean execution exists and makes at least one division.

Every pair has a complete actual beta-coded Euclidean execution, a genuinely certified gcd output, and the exact constructive linear bound steps <= initial divisor; the stronger BitLen bound remains open.