Constructive Euclidean gcd transport and anchored traces

Every witnessed common divisor of dividend and divisor also divides the exact Euclidean remainder.

Every witnessed common divisor of divisor and remainder also divides the exact Euclidean dividend.

Every constructive common divisor of (a,b) remains a common divisor of the next Euclidean pair (b,r).

Every constructive common divisor of (b,r) is already a common divisor of the previous Euclidean pair (a,b).

An exact bounded Euclidean division preserves the entire witnessed common-divisor relation in both constructive directions.

A relational gcd of the next Euclidean pair is a relational gcd of the previous exact pair.

A relational gcd of the previous exact Euclidean pair is a relational gcd of the next pair.

The full greatest-common-divisor specification is constructively equivalent before and after each exact Euclidean division.

Independently witnessed greatest common divisors before and after one exact Euclidean step are equal.

Any relational gcd at a zero-remainder terminal state is exactly its nonzero-side dividend, including a=0.

Any two Alpha-v21 Euclidean executions for the same input certify the same unique relational gcd output.

Two actual beta-history states at the same index have identical dividend, divisor, and encoded quotient list.

Natural induction over every actual beta-coded Euclidean transition preserves the gcd of the initial zero-divisor state at every history prefix.

The actual value encoded in the zeroth terminal Euclidean beta-state is a relational gcd of the original terminal input pair.

Every complete actual beta-coded Euclidean history contains a witnessed terminal zero state whose encoded value is the genuine gcd of its inputs.

The independently certified output of every Alpha-v21 EuclidExecution is exactly the natural encoded in its actual terminal zero-divisor beta state.

Every natural input pair has a genuine complete Euclidean beta execution whose actual terminal zero state is its certified gcd output.

Every pair has a complete actual beta-coded Euclidean execution whose terminal state is provably its gcd and whose exact step count satisfies steps <= b; the BitLen bound remains open.

Every anchored Euclidean execution independently satisfies the full original relational greatest-common-divisor specification.

Every anchored execution contains an actual complete beta history whose zeroth state encodes precisely the reported gcd value.