Certified logarithmic Euclidean algorithm — Exact Proof Explorer

Constructive natural doubling preserves witnessed non-strict order.

Strict comparison of two exact doubles constructively cancels the factor two.

A genuine two-step strict halving below twice a power lies below that power.

The exact two-step budget for a successor exponent grows by two.

Any actual complete Euclidean beta-history remains valid under one extra budget unit.

One actual strict Euclidean division extends a genuine bounded beta-history by exactly one step.

Two genuine consecutive Euclidean divisions extend a complete beta-history by exactly two steps.

A zero-divisor input has a genuine zero-step Euclidean history within every supplied budget.

An exact two-step budget is identically the doubled successor-exponent budget.

The zero Euclidean divisor is strictly below every witnessed power of two.

A natural strictly below the witnessed zeroth power of two must be zero.

Induction on a witnessed power of two constructs genuine complete Euclidean beta histories in at most twice the exponent, using strict halving across every actual pair of divisions.

Every genuine BitLen witness, including the zero-has-one-digit convention, supplies a witnessed strict upper power of two.

Every genuine BitLen witness constructively bounds an actual complete Euclidean beta history by twice its length.

Every bit-length witness constructs a genuine complete beta execution whose actual terminal state is its gcd and whose exact step count is at most twice that length.

Exact G101: every witnessed BitLen(b,l) yields a genuine gcd-anchored Euclidean beta execution with steps <= 2*l+1 in unchanged constructive HA.

For every pair of naturals construct all witnesses at once: canonical bit length, an actual terminal-gcd Euclidean beta execution, and the exact logarithmic step bound 2*BitLen(b)+1.