Bounded polynomial resultants

This file collects bridges used by exact-arithmetic polynomial certificates. The first transports a pseudo-remainder identity to bounded resultants. The remaining results turn a nonzero bounded resultant against a monic polynomial into the usual resultant, coprimality, and no-common-root conclusions, without requiring the left polynomial to retain its generic degree after specialization.

theorem MazurTorsion.PolynomialResultant.bounded_resultant_pseudoRemainder {R : Type u_1} [CommRing R] (a b q r : Polynomial R) (l c : R) (m n k delta : ℕ) (hb : b.natDegree ≤ n) (hr : r.natDegree ≤ k) (hq : q.natDegree + n ≤ m) (hkm : k ≤ m) (hbl : b.coeff n = l) (hid : Polynomial.C (l ^ delta) * a = Polynomial.C c * r + b * q) : l ^ (delta * n) * a.resultant b m n = (-1) ^ (n * (m - k)) * l ^ (m - k) * c ^ n * r.resultant b k n

A pseudo-remainder identity, with all degree padding explicit, induces the corresponding identity between bounded resultants.

theorem MazurTorsion.PolynomialResultant.resultant_telescope_33_7 {R : Type u_1} [CommRing R] [IsDomain R] (R0 R1 R2 R3 R4 R5 R6 L2 L3 L4 L5 L6 E0 E1 E2 E3 E4 E5 E6 U : R) (hL2 : L2 ≠ 0) (hL3 : L3 ≠ 0) (hL4 : L4 ≠ 0) (hL5 : L5 ≠ 0) (hL6 : L6 ≠ 0) (h0 : R0 = -E0 ^ 7 * R1) (h1 : L2 ^ 10 * R1 = E1 ^ 6 * R2) (h2 : L3 ^ 8 * R2 = L2 ^ 10 * E2 ^ 5 * R3) (h3 : L4 ^ 6 * R3 = L3 ^ 8 * E3 ^ 4 * R4) (h4 : L5 ^ 4 * R4 = L4 ^ 6 * E4 ^ 3 * R5) (h5 : L6 ^ 2 * R5 = L5 ^ 4 * E5 ^ 2 * R6) (h6 : R6 = L6 ^ 2 * E6 * U) : R0 = -E0 ^ 7 * E1 ^ 6 * E2 ^ 5 * E3 ^ 4 * E4 ^ 3 * E5 ^ 2 * E6 * U

Telescope for the bounded-resultant degree pattern 33, 7, 6, ..., 0.

The principal coefficients are cancelled in the coefficient domain, before the parameter is specialized. This is the algebraic cancellation used by the order-seven backtracking resultant certificate.

theorem MazurTorsion.PolynomialResultant.bounded_resultant_telescope_33_7 {R : Type u_1} [CommRing R] [IsDomain R] (r0 r1 r2 r3 r4 r5 r6 r7 r8 q0 q1 q2 q3 q4 q5 q6 : Polynomial R) (L2 L3 L4 L5 L6 L7 E0 E1 E2 E3 E4 E5 E6 U : R) (hr1 : r1.natDegree ≤ 7) (hr2 : r2.natDegree ≤ 6) (hr3 : r3.natDegree ≤ 5) (hr4 : r4.natDegree ≤ 4) (hr5 : r5.natDegree ≤ 3) (hr6 : r6.natDegree ≤ 2) (hr7 : r7.natDegree ≤ 1) (hr8 : r8.natDegree ≤ 0) (hq0 : q0.natDegree + 7 ≤ 33) (hq1 : q1.natDegree + 6 ≤ 7) (hq2 : q2.natDegree + 5 ≤ 6) (hq3 : q3.natDegree + 4 ≤ 5) (hq4 : q4.natDegree + 3 ≤ 4) (hq5 : q5.natDegree + 2 ≤ 3) (hq6 : q6.natDegree + 1 ≤ 2) (hlead1 : r1.coeff 7 = 1) (hlead2 : r2.coeff 6 = L2) (hlead3 : r3.coeff 5 = L3) (hlead4 : r4.coeff 4 = L4) (hlead5 : r5.coeff 3 = L5) (hlead6 : r6.coeff 2 = L6) (hlead7 : r7.coeff 1 = L7) (hL2 : L2 ≠ 0) (hL3 : L3 ≠ 0) (hL4 : L4 ≠ 0) (hL5 : L5 ≠ 0) (hL6 : L6 ≠ 0) (hL7 : L7 ≠ 0) (hrec0 : Polynomial.C (r1.coeff 7 ^ 27) * r0 = r1 * q0 + Polynomial.C E0 * r2) (hrec1 : Polynomial.C (r2.coeff 6 ^ 2) * r1 = r2 * q1 + Polynomial.C (r1.coeff 7 ^ 2 * E1) * r3) (hrec2 : Polynomial.C (r3.coeff 5 ^ 2) * r2 = r3 * q2 + Polynomial.C (r2.coeff 6 ^ 2 * E2) * r4) (hrec3 : Polynomial.C (r4.coeff 4 ^ 2) * r3 = r4 * q3 + Polynomial.C (r3.coeff 5 ^ 2 * E3) * r5) (hrec4 : Polynomial.C (r5.coeff 3 ^ 2) * r4 = r5 * q4 + Polynomial.C (r4.coeff 4 ^ 2 * E4) * r6) (hrec5 : Polynomial.C (r6.coeff 2 ^ 2) * r5 = r6 * q5 + Polynomial.C (r5.coeff 3 ^ 2 * E5) * r7) (hrec6 : Polynomial.C (r7.coeff 1 ^ 2) * r6 = r7 * q6 + Polynomial.C (r6.coeff 2 ^ 2 * E6) * r8) (hr8C : r8 = Polynomial.C U) : r0.resultant r1 33 7 = -E0 ^ 7 * E1 ^ 6 * E2 ^ 5 * E3 ^ 4 * E4 ^ 3 * E5 ^ 2 * E6 * U

The normalized bounded-resultant telescope for the degree pattern 33, 7, 6, 5, 4, 3, 2, 1, 0.

The recurrence hypotheses retain the generated leading coefficients, so an exact pseudo-remainder certificate can be passed without reshaping. All principal-coefficient cancellation happens over the coefficient domain.

theorem MazurTorsion.PolynomialResultant.resultant_ne_zero_of_bounded_resultant_ne_zero {R : Type u_1} [CommRing R] {f g : Polynomial R} {m n : ℕ} (hf : f.natDegree ≤ m) (hg : g.natDegree = n) (hmonic : g.Monic) (hres : f.resultant g m n ≠ 0) : f.resultant g ≠ 0

A nonzero bounded resultant against a monic polynomial is already a nonzero ordinary resultant. Only a degree bound is needed on the left polynomial, so this remains useful when specialization drops its degree.

theorem MazurTorsion.PolynomialResultant.isCoprime_of_bounded_resultant_ne_zero {K : Type u_2} [Field K] {f g : Polynomial K} {m n : ℕ} (hf : f.natDegree ≤ m) (hg : g.natDegree = n) (hmonic : g.Monic) (hres : f.resultant g m n ≠ 0) : IsCoprime f g

A nonzero bounded resultant against a monic polynomial over a field makes the two polynomials coprime.

theorem MazurTorsion.PolynomialResultant.bounded_resultant_ne_zero_of_isCoprime {K : Type u_2} [Field K] {f g : Polynomial K} {m n : ℕ} (hf : f.natDegree ≤ m) (hg : g.natDegree = n) (hmonic : g.Monic) (hcop : IsCoprime f g) : f.resultant g m n ≠ 0

Coprime polynomials have nonzero bounded resultant when the right polynomial is monic and the degree padding is explicit. The left polynomial may lose degree after specialization.

theorem MazurTorsion.PolynomialResultant.eval_ne_zero_or_eval_ne_zero_of_bounded_resultant_ne_zero {K : Type u_2} [Field K] {f g : Polynomial K} {m n : ℕ} (hf : f.natDegree ≤ m) (hg : g.natDegree = n) (hmonic : g.Monic) (hres : f.resultant g m n ≠ 0) (x : K) : Polynomial.eval x f ≠ 0 ∨ Polynomial.eval x g ≠ 0

A nonzero bounded resultant against a monic polynomial rules out a common root after specialization.