Twenty independently checked constructive theorems transport divisibility and gcd invariants through actual Euclidean steps, identify the terminal history state with its gcd, and establish a complete anchored linear bound.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
GT0001 · euclidean_divisor_remainder_transportEvery witnessed common divisor of dividend and divisor also divides the exact Euclidean remainder.
layer 0 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0002 · euclidean_divisor_dividend_transportEvery witnessed common divisor of divisor and remainder also divides the exact Euclidean dividend.
layer 0 · 17 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0003 · euclidean_common_divisor_forwardEvery constructive common divisor of (a,b) remains a common divisor of the next Euclidean pair (b,r).
layer 1 · 19 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0004 · euclidean_common_divisor_backwardEvery constructive common divisor of (b,r) is already a common divisor of the previous Euclidean pair (a,b).
layer 1 · 19 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0005 · euclidean_common_divisor_iffAn exact bounded Euclidean division preserves the entire witnessed common-divisor relation in both constructive directions.
layer 2 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0006 · euclidean_gcd_step_forwardA relational gcd of the next Euclidean pair is a relational gcd of the previous exact pair.
layer 0 · 16 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0007 · euclidean_gcd_step_backwardA relational gcd of the previous exact Euclidean pair is a relational gcd of the next pair.
layer 0 · 16 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0008 · euclidean_gcd_step_iffThe full greatest-common-divisor specification is constructively equivalent before and after each exact Euclidean division.
layer 1 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0009 · euclidean_gcd_step_output_uniqueIndependently witnessed greatest common divisors before and after one exact Euclidean step are equal.
layer 1 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT000A · euclidean_gcd_zero_terminal_uniqueAny relational gcd at a zero-remainder terminal state is exactly its nonzero-side dividend, including a=0.
layer 0 · 11 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT000B · euclidean_execution_output_uniqueAny two Alpha-v21 Euclidean executions for the same input certify the same unique relational gcd output.
layer 0 · 28 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT000C · euclidean_beta_state_functionalTwo actual beta-history states at the same index have identical dividend, divisor, and encoded quotient list.
layer 0 · 40 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT000D · euclidean_trace_prefix_gcd_invariantNatural induction over every actual beta-coded Euclidean transition preserves the gcd of the initial zero-divisor state at every history prefix.
layer 1 · 84 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT000E · euclidean_trace_initial_state_is_gcdThe actual value encoded in the zeroth terminal Euclidean beta-state is a relational gcd of the original terminal input pair.
layer 2 · 52 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT000F · euclidean_trace_terminal_gcd_existsEvery complete actual beta-coded Euclidean history contains a witnessed terminal zero state whose encoded value is the genuine gcd of its inputs.
layer 3 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0010 · euclidean_execution_terminal_identifiedThe independently certified output of every Alpha-v21 EuclidExecution is exactly the natural encoded in its actual terminal zero-divisor beta state.
layer 4 · 38 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0011 · euclidean_anchored_execution_existsEvery natural input pair has a genuine complete Euclidean beta execution whose actual terminal zero state is its certified gcd output.
layer 5 · 31 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0012 · euclidean_anchored_execution_linear_boundEvery 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.
layer 5 · 34 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0013 · euclidean_anchored_execution_gcd_correctEvery anchored Euclidean execution independently satisfies the full original relational greatest-common-divisor specification.
layer 0 · 11 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableGT0014 · euclidean_anchored_execution_state_correctEvery anchored execution contains an actual complete beta history whose zeroth state encodes precisely the reported gcd value.
layer 0 · 16 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 20 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.