def Hex.DensePoly.Subresultant.columnCofactorAt {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) (j : Fin (df - J + (dg - J))) : R

One column cofactor in a generalized coefficient matrix.

Equations

• Hex.DensePoly.Subresultant.columnCofactorAt df dg J f g j = Hex.SubresultantMinor.lastCofactor (Hex.DensePoly.Subresultant.coeffMatrixAt df dg J 0 f g) j

def Hex.DensePoly.Subresultant.cofactorUCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) : List (Fin (df - J + (dg - J))) → DensePoly R

Accumulate the left-block cofactor monomials over selected columns.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Subresultant.cofactorUCols df dg J f g [] = 0

def Hex.DensePoly.Subresultant.cofactorVCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) : List (Fin (df - J + (dg - J))) → DensePoly R

Accumulate the right-block cofactor monomials over selected columns.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Subresultant.cofactorVCols df dg J f g [] = 0

def Hex.DensePoly.Subresultant.cofactorRowCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) : List (Fin (df - J + (dg - J))) → DensePoly R

Sum the polynomial contribution of each selected Sylvester column.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Subresultant.cofactorRowCols df dg J f g [] = 0

def Hex.DensePoly.Subresultant.cofactorScalarCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) : List (Fin (df - J + (dg - J))) → R

Scalar final-row Laplace terms over selected Sylvester columns.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Subresultant.cofactorScalarCols df dg J l f g [] = 0

def Hex.DensePoly.Subresultant.blockCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (start count total : Nat) (p : DensePoly R) : List (Fin total) → DensePoly R

Reconstruct a bounded polynomial from a selected interval of coefficient columns, listed in descending monomial order.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Subresultant.blockCols start count total p [] = 0

def Hex.DensePoly.Subresultant.bezoutCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (u v f g : DensePoly R) : List (Fin (df - J + (dg - J))) → DensePoly R

Polynomial contribution of bounded left and right coefficient vectors.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Subresultant.bezoutCols df dg J u v f g [] = 0

def Hex.DensePoly.Subresultant.bezoutVector {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (u v : DensePoly R) : Vector R (df - J + (dg - J))

The bounded coefficient vector in Sylvester-column order.

Equations

• Hex.DensePoly.Subresultant.bezoutVector df dg J u v = Vector.ofFn fun (j : Fin (df - J + (dg - J))) => if ↑j < dg - J then u.coeff (dg - J - 1 - ↑j) else v.coeff (df - J - 1 - (↑j - (dg - J)))

def Hex.DensePoly.Subresultant.cofactorUAt {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) : DensePoly R

The cofactor polynomial contributed by the left (f) block at explicit formal degrees.

Equations

• Hex.DensePoly.Subresultant.cofactorUAt df dg J f g = Hex.DensePoly.Subresultant.cofactorUCols df dg J f g (List.finRange (df - J + (dg - J)))

def Hex.DensePoly.Subresultant.cofactorVAt {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) : DensePoly R

The cofactor polynomial contributed by the right (g) block at explicit formal degrees.

Equations

• Hex.DensePoly.Subresultant.cofactorVAt df dg J f g = Hex.DensePoly.Subresultant.cofactorVCols df dg J f g (List.finRange (df - J + (dg - J)))

def Hex.DensePoly.Subresultant.cofactorU {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (J : Nat) (f g : DensePoly R) : DensePoly R

The left Bezout cofactor of the J-th generalized subresultant.

Equations

• Hex.DensePoly.Subresultant.cofactorU J f g = Hex.DensePoly.Subresultant.cofactorUAt (Hex.DensePoly.Subresultant.formalDegree f) (Hex.DensePoly.Subresultant.formalDegree g) J f g

def Hex.DensePoly.Subresultant.cofactorV {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (J : Nat) (f g : DensePoly R) : DensePoly R

The right Bezout cofactor of the J-th generalized subresultant.

Equations

• Hex.DensePoly.Subresultant.cofactorV J f g = Hex.DensePoly.Subresultant.cofactorVAt (Hex.DensePoly.Subresultant.formalDegree f) (Hex.DensePoly.Subresultant.formalDegree g) J f g

theorem Hex.DensePoly.Subresultant.columnCofactorAt_eq {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) (j : Fin (df - J + (dg - J))) : columnCofactorAt df dg J f g j = SubresultantMinor.lastCofactor (coeffMatrixAt df dg J l f g) j

Column cofactors do not depend on the selected output coefficient, since that coefficient changes only the deleted final row.

theorem Hex.DensePoly.Subresultant.cofactorCols_mul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) (cols : List (Fin (df - J + (dg - J)))) : cofactorUCols df dg J f g cols * f + cofactorVCols df dg J f g cols * g = cofactorRowCols df dg J f g cols

The two accumulated cofactor blocks multiply back to the sum of their individual Sylvester-column contributions.

theorem Hex.DensePoly.Subresultant.blockCols_finRange {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (start count total : Nat) (p : DensePoly R) (hfit : start + count ≤ total) (hsize : p.size ≤ count) : blockCols start count total p (List.finRange total) = p

A full interval of reversed coefficient columns reconstructs the bounded polynomial.

theorem Hex.DensePoly.Subresultant.blockCols_mul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (u v f g : DensePoly R) (cols : List (Fin (df - J + (dg - J)))) : blockCols 0 (dg - J) (df - J + (dg - J)) u cols * f + blockCols (dg - J) (df - J) (df - J + (dg - J)) v cols * g = bezoutCols df dg J u v f g cols

The two reconstructed coefficient blocks multiply to their per-column Bezout contributions.

theorem Hex.DensePoly.Subresultant.bezoutCols_finRange {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (u v f g : DensePoly R) (hu : u.size ≤ dg - J) (hv : v.size ≤ df - J) : bezoutCols df dg J u v f g (List.finRange (df - J + (dg - J))) = u * f + v * g

Full bounded column lists reconstruct the original Bezout polynomial.

theorem Hex.DensePoly.Subresultant.coeff_bezoutCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (u v f g : DensePoly R) (hcount : 0 < df - J + (dg - J)) (cols : List (Fin (df - J + (dg - J)))) : (bezoutCols df dg J u v f g cols).coeff l = List.foldr (fun (j : Fin (df - J + (dg - J))) (acc : R) => coeffMatrixAt df dg J l f g ⟨df - J + (dg - J) - 1, ⋯⟩ j * (bezoutVector df dg J u v)[j] + acc) 0 cols

Coefficients of bounded Bezout columns are matrix-row products with the bounded coefficient vector.

theorem Hex.DensePoly.Subresultant.coeffMatrixAt_mul_bezoutVector_eq_zero {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J ell : Nat) (u v f g : DensePoly R) (hJ : J < dg) (hcount : 0 < df - J + (dg - J)) (hu : u.size ≤ dg - J) (hv : v.size ≤ df - J) (hzero : u * f + v * g = 0) : SubresultantMinor.toMatrix (coeffMatrixAt df dg J ell f g) * bezoutVector df dg J u v = 0

A bounded Bezout syzygy gives a kernel vector for every generalized coefficient matrix of the same index.

theorem Hex.DensePoly.Subresultant.bounded_bezout_unique {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (df dg J ell : Nat) (f g u v : DensePoly R) (hJ : J < dg) (hdet : coeffMinorAt df dg J ell f g ≠ 0) (hu : u.size ≤ dg - J) (hv : v.size ≤ df - J) (hzero : u * f + v * g = 0) : u = 0 ∧ v = 0

A nonzero generalized coefficient minor makes bounded Bezout representations unique.

theorem Hex.DensePoly.Subresultant.size_sub_le_max {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (p q : DensePoly R) : (p - q).size ≤ p.size.max q.size

A difference of dense polynomials is bounded by the larger operand size.

theorem Hex.DensePoly.Subresultant.cofactorUAt_size_le {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) : (cofactorUAt df dg J f g).size ≤ dg - J

Degree bound for the left determinantal cofactor block at explicit formal degrees.

theorem Hex.DensePoly.Subresultant.cofactorVAt_size_le {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J : Nat) (f g : DensePoly R) : (cofactorVAt df dg J f g).size ≤ df - J

Degree bound for the right determinantal cofactor block at explicit formal degrees.

theorem Hex.DensePoly.Subresultant.cofactorU_size_le {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (J : Nat) (f g : DensePoly R) : (cofactorU J f g).size ≤ formalDegree g - J

Degree bound for the canonical left cofactor at the actual formal degrees.

theorem Hex.DensePoly.Subresultant.cofactorV_size_le {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (J : Nat) (f g : DensePoly R) : (cofactorV J f g).size ≤ formalDegree f - J

Degree bound for the canonical right cofactor at the actual formal degrees.

theorem Hex.DensePoly.Subresultant.coeff_cofactorRowCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) (cols : List (Fin (df - J + (dg - J)))) : (cofactorRowCols df dg J f g cols).coeff l = cofactorScalarCols df dg J l f g cols

Each coefficient of the polynomial column sum is its scalar Laplace column sum.

theorem Hex.DensePoly.Subresultant.cofactorScalarCols_eq_laplace {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) (hcount : 0 < df - J + (dg - J)) (cols : List (Fin (df - J + (dg - J)))) : cofactorScalarCols df dg J l f g cols = List.foldr (fun (j : Fin (df - J + (dg - J))) (acc : R) => coeffMatrixAt df dg J l f g ⟨df - J + (dg - J) - 1, ⋯⟩ j * SubresultantMinor.lastCofactor (coeffMatrixAt df dg J l f g) j + acc) 0 cols

The scalar cofactor sum is the final-row Laplace sum of the coefficient matrix.

theorem Hex.DensePoly.Subresultant.cofactorScalarCols_finRange {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) (hcount : 0 < df - J + (dg - J)) : cofactorScalarCols df dg J l f g (List.finRange (df - J + (dg - J))) = coeffMinorAt df dg J l f g

At positive matrix dimension, the full scalar cofactor sum is the corresponding generalized coefficient minor.

theorem Hex.DensePoly.Subresultant.coeff_cofactorAt_mul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) (hcount : 0 < df - J + (dg - J)) : (cofactorUAt df dg J f g * f + cofactorVAt df dg J f g * g).coeff l = coeffMinorAt df dg J l f g

The accumulated cofactor products have the generalized determinant as every coefficient for which the coefficient matrix has positive dimension.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_eq_zero_of_lt {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg J l : Nat) (f g : DensePoly R) (hJ : J < dg) (hdg : dg ≤ df) (hf : f.size ≤ df + 1) (hg : g.size ≤ dg + 1) (hl : J < l) : coeffMinorAt df dg J l f g = 0

Coefficient minors above the requested subresultant degree vanish: in the active range their selector row repeats an earlier Sylvester row, and above that range the selector row is zero.

theorem Hex.DensePoly.Subresultant.cofactor_bezout {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (J : Nat) (f g : DensePoly R) (hgf : g.size ≤ f.size) (hJ : J < formalDegree g) : cofactorU J f g * f + cofactorV J f g * g = poly J f g

The determinantal cofactors give an integral Bezout representation of a generalized subresultant.

theorem Hex.DensePoly.Subresultant.eq_scaled_cofactor {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (J : Nat) (d : R) (f g u v : DensePoly R) (hgf : g.size ≤ f.size) (hJ : J < formalDegree g) (hroot : poly J f g ≠ 0) (hu : u.size ≤ formalDegree g - J) (hv : v.size ≤ formalDegree f - J) (hrepr : u * f + v * g = scale d (poly J f g)) : u = scale d (cofactorU J f g) ∧ v = scale d (cofactorV J f g)

Any bounded Bezout row for a scalar multiple of a nonzero subresultant is that scalar multiple of the determinantal cofactor row.