theorem HexBerlekampZassenhausMathlib.abs_det_le_row_l2norm_prod {N : ℕ} (A : Matrix (Fin N) (Fin N) ℤ) : |↑A.det| ≤ ∏ i : Fin N, √(∑ j : Fin N, ↑(A i j) ^ 2)

Hadamard's determinant bound specialized to integer matrices and Euclidean row norms.

theorem HexBerlekampZassenhausMathlib.abs_resultant_le_sylvester_row_l2norm_prod (f g : Polynomial ℤ) : |↑(f.resultant g)| ≤ ∏ i : Fin (f.natDegree + g.natDegree), √(∑ j : Fin (f.natDegree + g.natDegree), ↑(f.sylvester g f.natDegree g.natDegree i j) ^ 2)

Hadamard's bound applied to the Sylvester matrix defining the integer resultant.

theorem HexBerlekampZassenhausMathlib.resultant_natAbs_le_coeff_bound (f g : Polynomial ℤ) (A : ℕ) (hf : ∀ (k : ℕ), (f.coeff k).natAbs ≤ A) (hg : ∀ (k : ℕ), (g.coeff k).natAbs ≤ A) : (f.resultant g).natAbs ≤ ((f.natDegree + g.natDegree) * A) ^ (f.natDegree + g.natDegree)

A coefficientwise integer bound on two polynomials gives a completely elementary resultant bound. This is the Leibniz/Sylvester estimate used by the executable BHKS precision cap.

theorem HexBerlekampZassenhausMathlib.abs_det_le_col_l2norm_prod {N : ℕ} (A : Matrix (Fin N) (Fin N) ℤ) : |↑A.det| ≤ ∏ j : Fin N, √(∑ i : Fin N, ↑(A i j) ^ 2)

Hadamard's determinant bound in column form: bound the determinant by the product of column Euclidean norms. Obtained from the row form by transposing.

theorem HexBerlekampZassenhausMathlib.det_dvd_of_left_cols_dvd {d n : ℕ} (m : ℤ) (A : Matrix (Fin (d + n)) (Fin (d + n)) ℤ) (hcols : ∀ (j : Fin d) (i : Fin (d + n)), m ∣ A i (Fin.castAdd n j)) : m ^ d ∣ A.det

If the first d columns of an integer matrix are entrywise divisible by m, then m ^ d divides the determinant.

The Fin (d + n) indexing matches the two natural Sylvester column blocks: j.castAdd n addresses the left block of d columns, while the remaining columns are unconstrained.

theorem HexBerlekampZassenhausMathlib.det_dvd_of_cols_dvd {N d : ℕ} (m : ℤ) (A : Matrix (Fin N) (Fin N) ℤ) (cols : Fin d → Fin N) (hcols_inj : Function.Injective cols) (hcols : ∀ (j : Fin d) (i : Fin N), m ∣ A i (cols j)) : m ^ d ∣ A.det

If any specified d distinct columns of an integer matrix are entrywise divisible by m, then m ^ d divides the determinant.

theorem HexBerlekampZassenhausMathlib.dvd_resultant_of_sylvester_cols (f H : Polynomial ℤ) {d : ℕ} (m : ℤ) (A : Matrix (Fin (f.natDegree + H.natDegree)) (Fin (f.natDegree + H.natDegree)) ℤ) (cols : Fin d → Fin (f.natDegree + H.natDegree)) (hcols_inj : Function.Injective cols) (hdet : A.det = (f.sylvester H f.natDegree H.natDegree).det) (hcols : ∀ (j : Fin d) (i : Fin (f.natDegree + H.natDegree)), m ∣ A i (cols j)) : m ^ d ∣ f.resultant H

Abstract Sylvester-column valuation criterion for integer resultants.

If a determinant-preserving Sylvester column transformation produces d distinct columns whose entries are all divisible by m, then m ^ d divides the resultant. This is the determinant argument needed by the CLD/logarithmic derivative argument: downstream code supplies the transformed matrix and column divisibility witnesses directly, without assuming that the selected local factor divides the auxiliary polynomial modulo m.

theorem HexBerlekampZassenhausMathlib.pow_dvd_resultant_of_sylvester_cols {p k d : ℕ} (f H q : Polynomial ℤ) (_hq_monic : q.Monic) (_hq_deg : q.natDegree = d) (_hf_monic : f.Monic) (A : Matrix (Fin (f.natDegree + H.natDegree)) (Fin (f.natDegree + H.natDegree)) ℤ) (cols : Fin d → Fin (f.natDegree + H.natDegree)) (hcols_inj : Function.Injective cols) (hdet : A.det = (f.sylvester H f.natDegree H.natDegree).det) (hcols : ∀ (j : Fin d) (i : Fin (f.natDegree + H.natDegree)), ↑(p ^ k) ∣ A i (cols j)) : ↑(p ^ (k * d)) ∣ f.resultant H

Prime-power form of dvd_resultant_of_sylvester_cols.

The hypotheses deliberately mention only the Sylvester-column valuation data. For BHKS/CLD use, the selected monic local factor q of degree d explains where the d column directions come from, while the actual CLD coefficient congruences are packaged in hcols. No divisibility hypothesis q.map _ ∣ H.map _ is required.

theorem HexBerlekampZassenhausMathlib.det_updateCol_mulVec {R : Type u_1} [CommRing R] {N : ℕ} (A : Matrix (Fin N) (Fin N) R) (p : Fin N) (w : Fin N → R) : (A.updateCol p (A.mulVec w)).det = w p • A.det

Replacing a column of a square matrix by A.mulVec w; the linear combination of all columns with coefficients w; multiplies the determinant by the coefficient w p of the replaced column.

This is the determinant-preserving column-operation mechanism: when the replaced column appears in the combination with a unit coefficient (w p = 1, the monic-triangular case), the determinant is preserved exactly. It is the column-form repackaging of Matrix.det_updateCol_sum against mulVec.

theorem HexBerlekampZassenhausMathlib.abs_resultant_le_l2norm_pow (f g : Polynomial ℤ) : |↑(f.resultant g)| ≤ HexPolyZMathlib.l2norm f ^ g.natDegree * HexPolyZMathlib.l2norm g ^ f.natDegree

Mignotte-style coefficient bound on the integer resultant of two polynomials: bound the absolute value of Polynomial.resultant f g by the product of the polynomial coefficient l2norms, with the standard exponents appearing in BHKS.

theorem HexBerlekampZassenhausMathlib.int_resultant_ne_zero_of_coprime (f g : Polynomial ℤ) (h : IsCoprime f g) : f.resultant g ≠ 0

The upstream resultant nonvanishing theorem specialized to integer polynomials.

theorem HexBerlekampZassenhausMathlib.resultant_map_intCast_rat (f g : Polynomial ℤ) : (Polynomial.map (Int.castRingHom ℚ) f).resultant (Polynomial.map (Int.castRingHom ℚ) g) = ↑(f.resultant g f.natDegree g.natDegree)

Mapping an integer resultant to ℚ agrees with taking the resultant after mapping both input polynomials to ℚ.

theorem HexBerlekampZassenhausMathlib.int_resultant_eq_zero_iff_not_coprime_over_rat (f g : Polynomial ℤ) : f.resultant g = 0 ↔ (Polynomial.map (Int.castRingHom ℚ) f ≠ 0 ∨ Polynomial.map (Int.castRingHom ℚ) g ≠ 0) ∧ ¬IsCoprime (Polynomial.map (Int.castRingHom ℚ) f) (Polynomial.map (Int.castRingHom ℚ) g)

The integer resultant vanishes exactly when the rationally transported polynomials are nontrivially non-coprime.

theorem HexBerlekampZassenhausMathlib.int_resultant_ne_zero_of_coprime_over_rat (f g : Polynomial ℤ) (hcoprime : IsCoprime (Polynomial.map (Int.castRingHom ℚ) f) (Polynomial.map (Int.castRingHom ℚ) g)) : f.resultant g ≠ 0

Contrapositive form useful when the BHKS method proves coprimality after transporting an integer-polynomial pair to ℚ.

theorem HexBerlekampZassenhausMathlib.int_resultant_ne_zero_of_no_monic_irreducible_common_factor (f g : Polynomial ℤ) (hf_monic : f.Monic) (hcommon : ∀ (q : Polynomial ℤ), q.Monic → Irreducible q → q ∣ f → ¬q ∣ g) : f.resultant g ≠ 0

An integer resultant against a monic polynomial is nonzero when no monic irreducible integer factor of the first polynomial divides the second.

The proof extracts a monic irreducible factor of the rational gcd, descends it through Gauss's lemma, and uses monic division to descend divisibility of the possibly non-primitive second polynomial.

theorem HexBerlekampZassenhausMathlib.int_resultant_ne_zero_of_no_irreducible_common_factor (f g : Polynomial ℤ) (hf_ne : f ≠ 0) (hcommon : ∀ (q : Polynomial ℤ), Irreducible q → q ∣ f → ¬q ∣ g) : f.resultant g ≠ 0

An integer resultant against a nonzero polynomial is nonzero when no irreducible integer factor of the first polynomial divides the second.

This is the direct-coordinate form of int_resultant_ne_zero_of_no_monic_irreducible_common_factor: a primitive nonmonic input has no reason to admit monic integer factors. A hypothetical rational common factor is cleared of denominators, replaced by its primitive part, and descended through Gauss's lemma.

theorem HexBerlekampZassenhausMathlib.exists_witnesses_of_map_dvd_zmod {f q : Polynomial ℤ} {n : ℕ} (hdvd : Polynomial.map (Int.castRingHom (ZMod n)) q ∣ Polynomial.map (Int.castRingHom (ZMod n)) f) : ∃ (a : Polynomial ℤ) (r : Polynomial ℤ), f = q * a + Polynomial.C ↑n * r

Integer witnesses from a ZMod n divisibility of mapped integer polynomials. If q divides f after reducing both modulo n, then there are honest integer polynomial witnesses a, r with f = q * a + C n * r. No monicity hypothesis is needed: surjectivity of ℤ → ZMod n lifts the modular quotient, and the residual f - q * a is coefficientwise divisible by n.

theorem HexBerlekampZassenhausMathlib.mul_X_pow_mem_degreeLT_of_natDegree_lt {R : Type u_1} [Semiring R] (p : Polynomial R) {m t : ℕ} (hdeg : (p * Polynomial.X ^ t).natDegree < m) : p * Polynomial.X ^ t ∈ Polynomial.degreeLT R m

A shifted polynomial belongs to degreeLT when its natural degree is strictly below the bound.

theorem HexBerlekampZassenhausMathlib.neg_mul_X_pow_mem_degreeLT_of_natDegree_lt {R : Type u_1} [CommRing R] (p : Polynomial R) {m t : ℕ} (hdeg : (p * Polynomial.X ^ t).natDegree < m) : -p * Polynomial.X ^ t ∈ Polynomial.degreeLT R m

Negated shifted-polynomial version of mul_X_pow_mem_degreeLT_of_natDegree_lt, used by the left component of the common-factor Sylvester syzygy.

theorem HexBerlekampZassenhausMathlib.sylvesterMap_commonFactor_syzygy {R : Type u_1} [CommRing R] (q a b : Polynomial R) {m n t : ℕ} (hleft : -a * Polynomial.X ^ t ∈ Polynomial.degreeLT R m) (hright : b * Polynomial.X ^ t ∈ Polynomial.degreeLT R n) (hf : (q * a).natDegree ≤ m) (hg : (q * b).natDegree ≤ n) : ((q * a).sylvesterMap (q * b) hf hg) (⟨-a * Polynomial.X ^ t, hleft⟩, ⟨b * Polynomial.X ^ t, hright⟩) = 0

Common-factor syzygy for the Sylvester map.

If f = q * a and g = q * b, then the shifted pair (-a * X^t, b * X^t) is killed by the Sylvester map for (f, g). Later column-reduction work uses the q.natDegree shifts of this identity after reducing explicit quotient/remainder witnesses modulo m.

theorem HexBerlekampZassenhausMathlib.sylvesterMap_commonFactor_smul {R : Type u_1} [CommRing R] (q a b r s : Polynomial R) (c : R) {m n t : ℕ} (hleft : -a * Polynomial.X ^ t ∈ Polynomial.degreeLT R m) (hright : b * Polynomial.X ^ t ∈ Polynomial.degreeLT R n) (hf : (q * a + Polynomial.C c * r).natDegree ≤ m) (hg : (q * b + Polynomial.C c * s).natDegree ≤ n) : ↑(((q * a + Polynomial.C c * r).sylvesterMap (q * b + Polynomial.C c * s) hf hg) (⟨-a * Polynomial.X ^ t, hleft⟩, ⟨b * Polynomial.X ^ t, hright⟩)) = Polynomial.C c * ((r * b - s * a) * Polynomial.X ^ t)

Scalar-shifted common-factor syzygy for the Sylvester map.

When f and g share the factor q only after reducing modulo a scalar c ; recorded by the explicit witnesses f = q * a + C c * r and g = q * b + C c * s; the shifted pair (-a * X^t, b * X^t) is no longer killed by the Sylvester map, but its image is the scalar multiple C c * ((r * b - s * a) * X^t).

This is the correspondence from the exact syzygy sylvesterMap_commonFactor_syzygy (the c = 0 case) to the divisibility used by the column-reduction proof: the linear combination of Sylvester columns selected by (-a * X^t, b * X^t) is entrywise divisible by c. Taking t < q.natDegree shifts gives d independent such combinations.

theorem HexBerlekampZassenhausMathlib.sylvester_mulVec_commonFactor_smul {R : Type u_1} [CommRing R] (q a b r s : Polynomial R) (c : R) {m n t : ℕ} (hleft : -a * Polynomial.X ^ t ∈ Polynomial.degreeLT R m) (hright : b * Polynomial.X ^ t ∈ Polynomial.degreeLT R n) (hf : (q * a + Polynomial.C c * r).natDegree ≤ m) (hg : (q * b + Polynomial.C c * s).natDegree ≤ n) (i : Fin (m + n)) : ((q * a + Polynomial.C c * r).sylvester (q * b + Polynomial.C c * s) m n).mulVec (⇑((Polynomial.degreeLT.basisProd R m n).repr (⟨-a * Polynomial.X ^ t, hleft⟩, ⟨b * Polynomial.X ^ t, hright⟩))) i = c * ((r * b - s * a) * Polynomial.X ^ t).coeff ↑i

Each entry of the Sylvester column combination selected by the shifted common-factor direction (-a * X^t, b * X^t) is the scalar c times a fixed coefficient.

The coordinate vector of the direction in the product basis multiplies the Sylvester matrix to the coordinate vector of the image C c * ((r * b - s * a) * X^t) (sylvesterMap_commonFactor_smul), whose coefficients are visibly c-multiples. Hence the selected column combination is entrywise divisible by c: this is the per-entry input the determinant column-reduction needs once the q.natDegree shifts are assembled.

theorem HexBerlekampZassenhausMathlib.sylvester_commonFactor_colReduceStep {R : Type u_1} [CommRing R] (q a b r s : Polynomial R) (c : R) {m n t : ℕ} (hleft : -a * Polynomial.X ^ t ∈ Polynomial.degreeLT R m) (hright : b * Polynomial.X ^ t ∈ Polynomial.degreeLT R n) (hf : (q * a + Polynomial.C c * r).natDegree ≤ m) (hg : (q * b + Polynomial.C c * s).natDegree ≤ n) (p : Fin (m + n)) : have S := (q * a + Polynomial.C c * r).sylvester (q * b + Polynomial.C c * s) m n; have w := (Polynomial.degreeLT.basisProd R m n).repr (⟨-a * Polynomial.X ^ t, hleft⟩, ⟨b * Polynomial.X ^ t, hright⟩); (S.updateCol p (S.mulVec ⇑w)).det = w p • S.det ∧ ∀ (k : Fin (m + n)), c ∣ S.mulVec (⇑w) k

The monic-triangular column-reduction step for the Sylvester matrix.

Write w for the coordinate vector of the shifted common-factor direction (-a * X^t, b * X^t). Replacing column p of the Sylvester matrix S by the combination S.mulVec w (the syzygy column):

• multiplies the determinant by the pivot coefficient w p (det_updateCol_mulVec); in the monic-triangular case w p = 1 this is a determinant-preserving operation, and

• produces a column whose every entry is divisible by the scalar c (sylvester_mulVec_commonFactor_smul).

Assembling this step over the d = q.natDegree shifts t < d, with the pivots chosen so each w p = 1, gives the matrix A' of the column-reduction target: A'.det = S.det with d columns entrywise divisible by c. The remaining work is the bookkeeping that the chosen pivots carry unit coefficients (a leading coefficient of the cofactor, hence 1 under the monic hypothesis) and that the combinations reference only as-yet-unreplaced columns.

theorem HexBerlekampZassenhausMathlib.sylvester_mulVec_image {R : Type u_1} [CommRing R] (f g u w : Polynomial R) {m n : ℕ} (hu : u ∈ Polynomial.degreeLT R m) (hw : w ∈ Polynomial.degreeLT R n) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) (i : Fin (m + n)) : (f.sylvester g m n).mulVec (⇑((Polynomial.degreeLT.basisProd R m n).repr (⟨u, hu⟩, ⟨w, hw⟩))) i = (f * w + g * u).coeff ↑i

General Sylvester column-image identity.

The Sylvester matrix applied (mulVec) to the coordinate vector of a direction (u, w) in the product basis reads off, entry by entry, the coefficients of the image polynomial f * w + g * u under the Sylvester map. This is the direction-independent argument behind the common-factor specialisation sylvester_mulVec_commonFactor_smul: divisibility of a selected column combination reduces to divisibility of the coefficients of f * w + g * u.

theorem HexBerlekampZassenhausMathlib.sylvester_mulVec_cld_syzygy {R : Type u_1} [CommRing R] (f g q z : Polynomial R) (c : R) {m n t : ℕ} (hsyz : g * q - f * Polynomial.derivative q = Polynomial.C c * z) (hu : q * Polynomial.X ^ t ∈ Polynomial.degreeLT R m) (hw : -Polynomial.derivative q * Polynomial.X ^ t ∈ Polynomial.degreeLT R n) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) (i : Fin (m + n)) : c ∣ (f.sylvester g m n).mulVec (⇑((Polynomial.degreeLT.basisProd R m n).repr (⟨q * Polynomial.X ^ t, hu⟩, ⟨-Polynomial.derivative q * Polynomial.X ^ t, hw⟩))) i

Each entry of the Sylvester column combination selected by the CLD syzygy direction (q * X^t, -q' * X^t) is divisible by the scalar c.

The CLD syzygy hypothesis records that the monic selected factor q of f satisfies g * q - f * q' = C c * z; for the BHKS application c = p ^ k, f the input polynomial, g the auxiliary polynomial, and the congruence supplied by cldQuotientMod_congr_mul_derivative (rearranged so the divisor q does not have to divide the auxiliary polynomial g). The selected column combination is the coordinate image of (q * X^t, -q' * X^t), whose Sylvester image is (g * q - f * q') * X^t = C c * (z * X^t); visibly a c-multiple entrywise. This is the per-entry input the determinant column-reduction needs once the d = q.natDegree shifts t < d are assembled into the d selected columns.

theorem HexBerlekampZassenhausMathlib.basisProd_repr_castAdd {R : Type u_1} [CommRing R] {m n : ℕ} (p : ↥(Polynomial.degreeLT R m)) (w : ↥(Polynomial.degreeLT R n)) (i₁ : Fin m) : ((Polynomial.degreeLT.basisProd R m n).repr (p, w)) (Fin.castAdd n i₁) = (↑p).coeff ↑i₁

Value of degreeLT.basisProd's coordinate functional on a left-block index: the coordinate at i₁.castAdd n reads off the i₁-th coefficient of the first component.

theorem HexBerlekampZassenhausMathlib.basisProd_repr_natAdd {R : Type u_1} [CommRing R] {m n : ℕ} (p : ↥(Polynomial.degreeLT R m)) (w : ↥(Polynomial.degreeLT R n)) (i₂ : Fin n) : ((Polynomial.degreeLT.basisProd R m n).repr (p, w)) (Fin.natAdd m i₂) = (↑w).coeff ↑i₂

Value of degreeLT.basisProd's coordinate functional on a right-block index: the coordinate at i₂.natAdd m reads off the i₂-th coefficient of the second component.

noncomputable def HexBerlekampZassenhausMathlib.colReduceTransform {R : Type u_1} [CommRing R] (a b : Polynomial R) (m n d : ℕ) : Matrix (Fin (m + n)) (Fin (m + n)) R

The column-reduction transformation matrix for the common-factor Sylvester reduction.

In the natural Fin (m + n) Sylvester column layout, columns m + (n - d) .. m + n - 1 (the top d columns of the f-shift block) are the pivot columns. This matrix is the identity except on those d pivot columns, where column m + (n - d) + t carries the coordinate vector of the shifted common-factor direction (-a * X^t, b * X^t); its left m entries are the coefficients of -a * X^t, its right n entries those of b * X^t.

Multiplying the Sylvester matrix S on the right by this matrix replaces each pivot column by the syzygy combination S.mulVec (direction) while leaving the others fixed. The matrix is upper triangular with diagonal entry b.coeff (n-d) at each pivot (and 1 elsewhere), so det = (b.coeff (n-d)) ^ d; under a monic cofactor b this diagonal entry is 1 and the determinant is preserved.

Equations

• One or more equations did not get rendered due to their size.

theorem HexBerlekampZassenhausMathlib.colReduceTransform_blockTriangular {R : Type u_1} [CommRing R] (a b : Polynomial R) {m n d : ℕ} (hd : d ≤ n) (hb : b.natDegree + d ≤ n) : (colReduceTransform a b m n d).BlockTriangular id

colReduceTransform is upper triangular: below-diagonal entries vanish. The pivot columns are supported on rows ≤ the pivot because -a * X^t lives in degreeLT m (left block, all rows < m ≤ pivot) and b * X^t has degree ≤ (n - d) + t (right block, capped at the pivot row), using b.natDegree ≤ n - d.

theorem HexBerlekampZassenhausMathlib.colReduceTransform_det {R : Type u_1} [CommRing R] (a b : Polynomial R) {m n d : ℕ} (hd : d ≤ n) (hb : b.natDegree + d ≤ n) : (colReduceTransform a b m n d).det = b.coeff (n - d) ^ d

The determinant of colReduceTransform is (b.coeff (n - d)) ^ d.

theorem HexBerlekampZassenhausMathlib.colReduceTransform_pivot_col {R : Type u_1} [CommRing R] (a b : Polynomial R) {m n d : ℕ} (t : ℕ) (htd : t < d) (hdn : d ≤ n) (hl : -a * Polynomial.X ^ t ∈ Polynomial.degreeLT R m) (hr : b * Polynomial.X ^ t ∈ Polynomial.degreeLT R n) : (fun (k : Fin (m + n)) => colReduceTransform a b m n d k (Fin.natAdd m ⟨n - d + t, ⋯⟩)) = ⇑((Polynomial.degreeLT.basisProd R m n).repr (⟨-a * Polynomial.X ^ t, hl⟩, ⟨b * Polynomial.X ^ t, hr⟩))

The pivot column m + (n - d) + t of colReduceTransform is the coordinate vector of the shifted common-factor direction (-a * X^t, b * X^t) in degreeLT.basisProd.

theorem HexBerlekampZassenhausMathlib.sylvester_commonFactor_colReduce {R : Type u_1} [CommRing R] (q a b r s : Polynomial R) (c : R) {m n d : ℕ} (hd : d ≤ n) (ha : a.natDegree + d ≤ m) (hb : b.natDegree + d ≤ n) (hf : (q * a + Polynomial.C c * r).natDegree ≤ m) (hg : (q * b + Polynomial.C c * s).natDegree ≤ n) : ((q * a + Polynomial.C c * r).sylvester (q * b + Polynomial.C c * s) m n * colReduceTransform a b m n d).det = b.coeff (n - d) ^ d * ((q * a + Polynomial.C c * r).sylvester (q * b + Polynomial.C c * s) m n).det ∧ ∀ (t : Fin d) (i : Fin (m + n)), c ∣ ((q * a + Polynomial.C c * r).sylvester (q * b + Polynomial.C c * s) m n * colReduceTransform a b m n d) i (Fin.natAdd m ⟨n - d + ↑t, ⋯⟩)

Assembled common-factor column reduction for the Sylvester matrix.

Write S = sylvester (q*a + C c*r) (q*b + C c*s) m n for the Sylvester matrix of two polynomials sharing the factor q modulo the scalar c (recorded by the explicit witnesses f = q*a + C c*r, g = q*b + C c*s). Right-multiplying S by colReduceTransform a b m n d produces a matrix A' whose

• determinant is (b.coeff (n - d)) ^ d * S.det; the cofactor leading coefficient raised to the d = q.natDegree shifts; under a monic cofactor b (so b.coeff (n - d) = 1) this is exactly S.det, and

• top d f-shift columns (the pivots m + (n - d) + t for t : Fin d) are entrywise divisible by c.

This is the matrix A' that #6858 feeds to det_dvd_of_left_cols_dvd (after a column reindex moving the d divisible columns to the front) to obtain c ^ d ∣ S.det = ± resultant. The degree side conditions a.natDegree + d ≤ m, b.natDegree + d ≤ n are the natural cofactor-degree bounds (deg a = m - d, deg b = n - d); hf, hg bound the witnessed polynomials.

theorem HexBerlekampZassenhausMathlib.commonFactor_dvd_resultant (f g q a b r s : Polynomial ℤ) (m : ℤ) {d : ℕ} (hf_wit : f = q * a + Polynomial.C m * r) (hg_wit : g = q * b + Polynomial.C m * s) (hq_monic : q.Monic) (hq_deg : q.natDegree = d) (hd : d ≤ g.natDegree) (ha : a.natDegree + d ≤ f.natDegree) (hb : b.natDegree + d ≤ g.natDegree) (hb_pivot : IsCoprime m (b.coeff (g.natDegree - d))) : m ^ d ∣ f.resultant g

Explicit-witness common-factor divisibility for integer resultants.

If f and g share a monic degree-d factor q modulo m, recorded by integer witnesses f = q*a + C m*r and g = q*b + C m*s, and the cofactor pivot is coprime to m, then m ^ d divides the integer resultant. The column transform contributes pivot ^ d; coprimality cancels that harmless factor from the determinant divisibility.

theorem HexBerlekampZassenhausMathlib.commonFactor_dvd_resultant_of_monic_cofactor (f g q a b r s : Polynomial ℤ) (m : ℤ) {d : ℕ} (hf_wit : f = q * a + Polynomial.C m * r) (hg_wit : g = q * b + Polynomial.C m * s) (hq_monic : q.Monic) (hq_deg : q.natDegree = d) (hd : d ≤ g.natDegree) (ha : a.natDegree + d ≤ f.natDegree) (hb_degree : b.natDegree + d = g.natDegree) (hb_monic : b.Monic) : m ^ d ∣ f.resultant g

Monic-cofactor form of commonFactor_dvd_resultant: if the right cofactor b is monic and has the expected degree g.natDegree - d, then the pivot coefficient required by the column reduction is automatically 1.

theorem HexBerlekampZassenhausMathlib.pow_dvd_resultant_of_map_dvd {p k : ℕ} {f g q : Polynomial ℤ} {d : ℕ} (hq_monic : q.Monic) (hq_deg : q.natDegree = d) (hf_ne : f ≠ 0) (hf_lc_coprime : IsCoprime (↑(p ^ k)) f.leadingCoeff) (hdf : d ≤ f.natDegree) (hdg : d ≤ g.natDegree) (hf_dvd : Polynomial.map (Int.castRingHom (ZMod (p ^ k))) q ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ k))) f) (hg_dvd : Polynomial.map (Int.castRingHom (ZMod (p ^ k))) q ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ k))) g) : ↑(p ^ (k * d)) ∣ f.resultant g

BHKS Lemma 3.2 modular-resultant divisibility, in the form downstream Hensel/CLD code consumes.

If a monic degree-d polynomial q divides both f and g after reduction modulo p ^ k, with the leading coefficient of nonzero f a unit modulo p ^ k and d not exceeding either degree, then p ^ (k * d) divides the integer resultant of f and g.

The exponent is k * d, not merely k: the monic common factor q contributes d independent Sylvester column directions, each carrying one factor of the modulus p ^ k, so the column reduction (commonFactor_dvd_resultant) turns those d directions into (p ^ k) ^ d = p ^ (k * d) dividing the resultant. The leading coefficient of f supplies the coprime pivot the reduction needs; the result is read off the swapped pair via Polynomial.resultant_comm.

theorem HexBerlekampZassenhausMathlib.pow_dvd_resultant_of_map_dvd_left_coprime {p k : ℕ} {f g q : Polynomial ℤ} {d : ℕ} (hmod : 1 < p ^ k) (hq_monic : q.Monic) (hq_deg : q.natDegree = d) (hf_ne : f ≠ 0) (hf_lc_coprime : IsCoprime (↑(p ^ k)) f.leadingCoeff) (hdf : d ≤ f.natDegree) (hf_dvd : Polynomial.map (Int.castRingHom (ZMod (p ^ k))) q ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ k))) f) (hg_dvd : Polynomial.map (Int.castRingHom (ZMod (p ^ k))) q ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ k))) g) : ↑(p ^ (k * d)) ∣ f.resultant g

Common-factor resultant divisibility without an auxiliary-degree hypothesis.

If the auxiliary has degree at least the monic modular common factor, this is pow_dvd_resultant_of_map_dvd. Otherwise modular divisibility by that monic factor forces the entire auxiliary to vanish modulo p^k; hence it is a scalar multiple of p^k, and resultant homogeneity supplies at least d copies of that scalar because d ≤ f.natDegree.

noncomputable def HexBerlekampZassenhausMathlib.cldColReduceTransform {R : Type u_1} [CommRing R] (q : Polynomial R) (m n d : ℕ) : Matrix (Fin (m + n)) (Fin (m + n)) R

The CLD-syzygy column-reduction transform for the Sylvester matrix.

In the Fin (m + n) layout of sylvester f g m n, the left block columns d, d+1, …, 2d-1 are the pivot columns. Column d + t carries the coordinate vector of the shifted CLD-syzygy direction (q * X^t, -q' * X^t) in degreeLT.basisProd: its left m entries are the coefficients of the monic q * X^t, its right n entries those of -q' * X^t. Every other column is the identity column.

Right-multiplying sylvester f g m n by this matrix replaces each pivot column with the syzygy combination S.mulVec (direction) (entrywise divisible by the syzygy scalar, via sylvester_mulVec_cld_syzygy) while leaving the others fixed. The matrix is block-lower-triangular for the left/right partition; its top-right block vanishes because the right columns stay identity; and its left diagonal block is upper triangular with the monic leading 1 of q * X^t on the diagonal, so det = 1. Unlike colReduceTransform, the monic pivot here is the left component q, so the matrix is not triangular under the natural order; the determinant is read off the block decomposition.

Equations

• One or more equations did not get rendered due to their size.

theorem HexBerlekampZassenhausMathlib.cldColReduceTransform_det {R : Type u_1} [CommRing R] (q : Polynomial R) {m n d : ℕ} (hq_monic : q.Monic) (hq_deg : q.natDegree = d) : (cldColReduceTransform q m n d).det = 1

The determinant of cldColReduceTransform is 1: the left diagonal block is upper triangular with the monic leading coefficient of q on its diagonal, and the top-right block vanishes (the right columns are identity).

theorem HexBerlekampZassenhausMathlib.cldColReduceTransform_pivot_col {R : Type u_1} [CommRing R] (q : Polynomial R) {m n d : ℕ} (t : ℕ) (htd : t < d) (htm : d + t < m) (hl : q * Polynomial.X ^ t ∈ Polynomial.degreeLT R m) (hr : -Polynomial.derivative q * Polynomial.X ^ t ∈ Polynomial.degreeLT R n) : (fun (k : Fin (m + n)) => cldColReduceTransform q m n d k (Fin.castAdd n ⟨d + t, htm⟩)) = ⇑((Polynomial.degreeLT.basisProd R m n).repr (⟨q * Polynomial.X ^ t, hl⟩, ⟨-Polynomial.derivative q * Polynomial.X ^ t, hr⟩))

The pivot column d + t (in the left block) of cldColReduceTransform is the coordinate vector of the shifted CLD-syzygy direction (q * X^t, -q' * X^t) in degreeLT.basisProd.

theorem HexBerlekampZassenhausMathlib.cld_syzygy_dvd_resultant (f g q z : Polynomial ℤ) (c : ℤ) {d : ℕ} (hq_monic : q.Monic) (hq_deg : q.natDegree = d) (hsyz : g * q - f * Polynomial.derivative q = Polynomial.C c * z) (hf_deg : 2 * d ≤ f.natDegree) (hg_deg : 2 * d ≤ g.natDegree + 1) : c ^ d ∣ f.resultant g

CLD-syzygy resultant divisibility (BHKS Lemma 3.2, scalar form).

If a monic degree-d polynomial q and a witness z record the CLD syzygy g * q - f * q' = C c * z, then c ^ d divides the integer resultant of f and g. Crucially, no divisibility hypothesis q ∣ g (or its modular form) is assumed: the syzygy provides d Sylvester column directions (q * X^t, -q' * X^t) whose images are c-multiples, and the monic leading 1 of each q * X^t makes the column-reduction transform determinant-preserving.

The degree bounds are intrinsic to the syzygy method: the d shifts of q * X^t must lie in degreeLT f.natDegree (forcing 2 * d ≤ f.natDegree), and the d shifts of -q' * X^t must lie in degreeLT g.natDegree (forcing 2 * d ≤ g.natDegree + 1). The first is the deg input ≥ 2d constraint flagged in BHKS Lemma 3.2; the second is the analogous bound on the auxiliary-polynomial degree, which downstream callers must also discharge (or fall back to the cut-based argument for small factors).

theorem HexBerlekampZassenhausMathlib.cld_syzygy_pow_dvd_resultant {p k : ℕ} (f g q z : Polynomial ℤ) {d : ℕ} (hq_monic : q.Monic) (hq_deg : q.natDegree = d) (hsyz : g * q - f * Polynomial.derivative q = Polynomial.C ↑(p ^ k) * z) (hf_deg : 2 * d ≤ f.natDegree) (hg_deg : 2 * d ≤ g.natDegree + 1) : ↑(p ^ (k * d)) ∣ f.resultant g

Prime-power form of cld_syzygy_dvd_resultant (BHKS Lemma 3.2, as consumed by the Hensel/CLD layer). With the syzygy scalar c = p ^ k, the d column directions each carry one factor of p ^ k, so p ^ (k * d) divides the resultant. No hypothesis that the selected factor divides the auxiliary polynomial modulo p ^ k is required.