Actual Euclidean descent · normalized gcd · formal uniqueness · Constructive arithmetic

Prime-Field Polynomial GCD and Bézout

Prime(p) ∧ Coeff(A) ∧ Coeff(B) ⇒ ∃ G U V. NormalizedGcd(G,A,B) ∧ Bezout(A,B,G,U,V)

Construct a zero-or-monic greatest common right divisor with actual Bézout coefficients over every prime field, including empty and all-zero inputs.

Open the definition-aware map Read the final theorem See campaign milestone G091

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 certificate

Fully expanded arithmetic

Inspect all 12211 native tactic lines and 543 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PG006B and follow only the lemmas and conservative definitions supporting prime_field_polynomial_bezout_is_right_gcd.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G091 milestone → theorem and definition dependencies.
Major independently established statements: PG000D prime_field_polynomial_convolution_shift_right_exists · PG0017 prime_field_polynomial_convolution_right_scale_exists · PG0019 prime_field_polynomial_convolution_right_scale_zero · PG001C prime_field_convolution_coefficient_right_append_add · PG001F prime_field_polynomial_convolution_right_append_exists · PG0028 prime_field_polynomial_right_divides_dividend_bounded · PG0034 prime_field_polynomial_right_divides_reflexive · PG0044 prime_field_polynomial_aligned_subtract_from_fixed · PG0048 prime_field_polynomial_aligned_subtract_functional · PG0050 prime_field_polynomial_left_constant_product_to_scale · PG0054 prime_field_polynomial_division_constant_remainder_empty · PG006C prime_field_polynomial_normalized_gcd_bezout_exists · PG0077 prime_field_polynomial_normalized_gcd_equivalent_unique · PG006B prime_field_polynomial_bezout_is_right_gcd.
Independently verified Alpha v34 checked-use theorem family: 119 dependency-curried kernel-checked theorem bodies · 543 proof prerequisites · 45 linked definitions · 93 definition-dependency arrows · 12211 exact tactic lines · first admitted v34 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 493 bundle nodes; SHA-256 3fe18ad2899cff7db5fbe19df8570ef70b1bfb902171d5212e9b036dda660a46.
Exact mathematical boundary: All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.