Bridge: synthetic linear division equals general monic division

Proves that the bespoke synthetic division divByLinearY Q f (Horner) coincides with general monic Euclidean division of Q by the linear factor Y - f, using the CommRing-general CPolynomial.divByMonic / CPolynomial.modByMonic at the coefficient ring CPolynomial R (recall CBivariate R = CPolynomial (CPolynomial R)).

divByLinearY_eq_divByMonic shows the quotient equals (divByLinearY Q f).1 and the remainder equals CPolynomial.C (divByLinearY Q f).2, so divByLinearY is a verified fast path for division by Y - f.

The proof works in the outer polynomial ring (CPolynomial R)[Y] (the image of CPolynomial.toPoly): it rewrites the divisor as X - C f (linearYDivisor_toPoly), establishes the Euclidean identity by transporting divByLinearY_spec across the coefficient ring-equiv (divByLinearY_euclid_toPoly), and concludes via Polynomial.div_modByMonic_unique.

def CompPoly.CBivariate.linearYDivisor {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (f : CPolynomial R) : CBivariate R

The linear monic divisor Y - f, as a bivariate polynomial (CBivariate R = CPolynomial (CPolynomial R)).

theorem CompPoly.CBivariate.linearYDivisor_toPoly {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CPolynomial R) : CPolynomial.toPoly (linearYDivisor f) = Polynomial.X - Polynomial.C f

toPoly sends the linear divisor Y - f to X - C f in (CPolynomial R)[Y].

theorem CompPoly.CBivariate.linearYDivisor_monic {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CPolynomial R) : CPolynomial.monic (linearYDivisor f) = true

The linear divisor Y - f is monic.

theorem CompPoly.CBivariate.divByLinearY_euclid_toPoly {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (f : CPolynomial R) : (CPolynomial.C (Q.divByLinearY f).2).toPoly + CPolynomial.toPoly (linearYDivisor f) * CPolynomial.toPoly (Q.divByLinearY f).1 = CPolynomial.toPoly Q

Euclidean identity for divByLinearY in the outer ring (CPolynomial R)[Y]: C rem + (Y - f) * quot = Q after toPoly. Transports divByLinearY_spec across the coefficient ring-equiv.

theorem CompPoly.CBivariate.divByLinearY_eq_divByMonic {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (f : CPolynomial R) : CPolynomial.divByMonic Q (linearYDivisor f) = (Q.divByLinearY f).1 ∧ CPolynomial.modByMonic Q (linearYDivisor f) = CPolynomial.C (Q.divByLinearY f).2

The bespoke synthetic division divByLinearY agrees with general monic division by Y - f: the quotient matches divByMonic, and the constant-in-Y remainder C (divByLinearY Q f).2 matches modByMonic.