Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Bézout identity and the Euclidean algorithm for polynomials over a field
Statement
Let be a field and let be not both zero. Repeated polynomial division terminates at a last nonzero remainder, whose monic associate is . There are such that
Moreover, divides both and , and every common divisor of and divides .
Facts & Assumptions
Given: A field and polynomials not both zero.
The monic gcd is the monic generator of the ideal (The monic greatest common divisor of two polynomials over a field).
Division by a nonzero polynomial over a field gives a unique remainder of smaller degree or zero (Division algorithm for polynomials over a field).
Proof
If necessary interchange and so the second input is nonzero. Repeatedly apply [L2]; this also covers a zero first input, when the first remainder is already zero. Each nonzero remainder has strictly smaller natural degree than its divisor, so the process terminates. Every remainder is a polynomial linear combination of the original by back-substitution, and the last nonzero remainder divides the preceding remainder and hence, successively, both inputs.
Every common divisor of divides each remainder and therefore divides ; after multiplying and its back-substituted coefficients by , the resulting monic polynomial has the divisibility property and generates , so [L1] identifies it with .