def Hex.SubresultantMinor.productCol {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] {n : Nat} (M : Square R n) (dst : Fin n) (db offset : Nat) (hsrc : db + offset < ↑dst) (b : DensePoly R) (i : Fin n) (count : Nat) : count ≤ db + 1 → R

The value of one destination column after adding the first count multiplier terms.

Equations

• Hex.SubresultantMinor.productCol M dst db offset hsrc b i 0 x_2 = M i dst
• Hex.SubresultantMinor.productCol M dst db offset hsrc b i count.succ h = Hex.SubresultantMinor.productCol M dst db offset hsrc b i count ⋯ + b.coeff count * M i ⟨db + offset - count, ⋯⟩

def Hex.SubresultantMinor.addProduct {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] {n : Nat} (M : Square R n) (dst : Fin n) (db offset : Nat) (hsrc : db + offset < ↑dst) (b : DensePoly R) (count : Nat) : count ≤ db + 1 → Square R n

Add the first count multiplier terms to one destination column.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SubresultantMinor.addProduct M dst db offset hsrc b 0 x_2 = M

theorem Hex.SubresultantMinor.addProduct_apply {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] {n : Nat} (M : Square R n) (dst : Fin n) (db offset : Nat) (hsrc : db + offset < ↑dst) (b : DensePoly R) (count : Nat) (h : count ≤ db + 1) (i j : Fin n) : addProduct M dst db offset hsrc b count h i j = if j = dst then productCol M dst db offset hsrc b i count h else M i j

Entrywise action of the multiplier-coefficient additions for one destination.

theorem Hex.SubresultantMinor.det_addProduct {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] {n : Nat} (M : Square R n) (dst : Fin n) (db offset : Nat) (hsrc : db + offset < ↑dst) (b : DensePoly R) (count : Nat) (h : count ≤ db + 1) : det (addProduct M dst db offset hsrc b count h) = det M

One multiplier-column update preserves the local determinant.

def Hex.SubresultantMinor.productCols {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] {n : Nat} (M : Square R n) (split db : Nat) (b : DensePoly R) (right : Nat) : db + right ≤ split → split + right ≤ n → Square R n

Apply the Brown multiplier update to right consecutive columns starting at split. Sources stay strictly to the left of split, so no destination is ever read as a source.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SubresultantMinor.productCols M split db b 0 x_3 x_4 = M

theorem Hex.SubresultantMinor.productCols_apply {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] {n : Nat} (M : Square R n) (split db : Nat) (b : DensePoly R) (right : Nat) (hs : db + right ≤ split) (ht : split + right ≤ n) (i j : Fin n) : productCols M split db b right hs ht i j = if hj : split ≤ ↑j ∧ ↑j < split + right then productCol M j db (↑j - split) ⋯ b i (db + 1) ⋯ else M i j

Entrywise action of the complete Brown multiplier-column update.

theorem Hex.SubresultantMinor.det_productCols {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] {n : Nat} (M : Square R n) (split db : Nat) (b : DensePoly R) (right : Nat) (hs : db + right ≤ split) (ht : split + right ≤ n) : det (productCols M split db b right hs ht) = det M

The complete Brown multiplier-column update preserves the determinant.

def Hex.DensePoly.Subresultant.coeffFold {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (b g : DensePoly R) (t : Int) (count : Nat) : R

The first count terms of the coefficient convolution of b and g at an integer index. Negative indices of g contribute zero.

Equations

• Hex.DensePoly.Subresultant.coeffFold b g t count = List.foldl (fun (acc : R) (k : Nat) => acc + b.coeff k * Hex.DensePoly.Subresultant.coeffInt g (t - ↑k)) 0 (List.range count)

theorem Hex.DensePoly.Subresultant.coeffFold_succ {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (b g : DensePoly R) (t : Int) (count : Nat) : coeffFold b g t (count + 1) = coeffFold b g t count + b.coeff count * coeffInt g (t - ↑count)

Extending the convolution fold appends the next coefficient product.

theorem Hex.DensePoly.Subresultant.coeffFold_of_size_le {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (b g : DensePoly R) (t : Int) (count : Nat) (h : b.size ≤ count) : coeffFold b g t count = coeffFold b g t b.size

Extending the convolution past the stored size of the left factor only adds zero coefficients.

theorem Hex.DensePoly.Subresultant.coeffFold_eq_mul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (b g : DensePoly R) (t : Int) : coeffFold b g t b.size = coeffInt (b * g) t

The full integer-indexed coefficient fold is the corresponding product coefficient.

theorem Hex.DensePoly.Subresultant.coeffInt_add_mul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (f b g : DensePoly R) (t : Int) : coeffInt (f + b * g) t = coeffInt f t + coeffFold b g t b.size

Brown's polynomial update is coefficientwise the original coefficient plus the multiplier convolution.

theorem Hex.DensePoly.Subresultant.productCols_addMul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg db J l : Nat) (f g b h : DensePoly R) (hJ : J < dg) (hdeg : df = db + dg) (hb : b.size ≤ db + 1) (hh : h = f + b * g) : SubresultantMinor.productCols (coeffMatrixAt dg df J l g f) (df - J) db b (dg - J) ⋯ ⋯ = coeffMatrixAt dg df J l g h

Brown's unit upper-triangular column transformation turns the swapped generalized Sylvester matrix for G, F into the coefficient matrix with blocks G, H, where H = F + B * G.

theorem Hex.DensePoly.Subresultant.det_addMul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg db J l : Nat) (f g b h : DensePoly R) (hJ : J < dg) (hdeg : df = db + dg) (hb : b.size ≤ db + 1) (hh : h = f + b * g) : SubresultantMinor.det (coeffMatrixAt dg df J l g h) = SubresultantMinor.det (coeffMatrixAt dg df J l g f)

The Brown column transformation preserves the determinant of the swapped generalized Sylvester matrix.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_addMul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg db J l : Nat) (f g b h : DensePoly R) (hJ : J < dg) (hdeg : df = db + dg) (hb : b.size ≤ db + 1) (hh : h = f + b * g) : coeffMinorAt df dg J l f g = SubresultantMinor.sign ((df - J) * (dg - J)) * coeffMinorAt dg df J l g h

The column-operation form of Brown--Traub equation (18): after swapping the input blocks, a unit upper-triangular transformation replaces F by H = F + B * G and leaves only the usual block-swap sign.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_succRight {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (dg dh J l : Nat) (g h : DensePoly R) (hpos : 0 < dg - J + (dh - J)) (hJh : J ≤ dh) (hg : g.size = dg + 1) (hh : h.size ≤ dh + 1) : coeffMinorAt dg (dh + 1) J l g h = g.leadingCoeff * coeffMinorAt dg dh J l g h

Raising the retained formal degree of the right input by one contributes one leading coefficient of the left input, provided the right polynomial has no coefficient at the new degree. This is used in the opposite direction to collapse an artificially retained formal degree.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_raiseRight {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (dg dh J l extra : Nat) (g h : DensePoly R) (hpos : 0 < dg - J + (dh - J)) (hJh : J ≤ dh) (hg : g.size = dg + 1) (hh : h.size ≤ dh + 1) : coeffMinorAt dg (dh + extra) J l g h = g.leadingCoeff ^ extra * coeffMinorAt dg dh J l g h

Raising the retained formal degree of the right input repeatedly contributes the corresponding power of the left leading coefficient. Reading the equality right-to-left collapses all retained degrees at once.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_leftSucc {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (dh l : Nat) (g h : DensePoly R) : coeffMinorAt (dh + 1) dh dh l g h = h.coeff l

When the right formal degree is one below the left and the subresultant index equals it, the one-entry coefficient minor selects the right input.

theorem Hex.DensePoly.Subresultant.poly_prem {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g : DensePoly R) (hgsize : 2 ≤ g.size) (hgf : g.size ≤ f.size) : poly (g.size - 2) f g = scale (SubresultantMinor.sign (f.size - g.size + 1)) (f.pseudoDivMod g).snd

The subresultant immediately below the divisor degree is the signed pseudo-remainder. This includes defective remainders: no exact degree is assumed for the remainder.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_rightDegree {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (dg dh l : Nat) (g h : DensePoly R) (hdh : dh < dg) (hh : h.size = dh + 1) : coeffMinorAt dg dh dh l g h = h.leadingCoeff ^ (dg - dh - 1) * h.coeff l

The subresultant at the right input's degree is that input multiplied by the expected power of its leading coefficient.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_brownTraub {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg db dh J l : Nat) (f g b h : DensePoly R) (hJh : J ≤ dh) (hdh : dh < dg) (hdeg : df = db + dg) (hg : g.size = dg + 1) (hb : b.size ≤ db + 1) (hhsize : h.size ≤ dh + 1) (hh : h = f + b * g) : coeffMinorAt df dg J l f g = SubresultantMinor.sign ((df - J) * (dg - J)) * (g.leadingCoeff ^ (df - dh) * coeffMinorAt dg dh J l g h)

Brown--Traub equation (12): if H = F + B * G, then the generalized Sylvester coefficient minor for F, G is the G, H minor at any formal degree bounding H, times the block-swap sign and one lc(G) for every collapsed formal degree.

theorem Hex.DensePoly.Subresultant.poly_rightDegree {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (dg dh : Nat) (g h : DensePoly R) (hdh : dh < dg) (hg : g.size = dg + 1) (hh : h.size = dh + 1) : poly dh g h = scale (h.leadingCoeff ^ (dg - dh - 1)) h

The generalized subresultant at the right input's degree is a scalar multiple of that input.

theorem Hex.DensePoly.Subresultant.poly_brownTraub {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg db dh J : Nat) (f g b h : DensePoly R) (hJh : J ≤ dh) (hdh : dh < dg) (hdeg : df = db + dg) (hf : f.size = df + 1) (hg : g.size = dg + 1) (hb : b.size ≤ db + 1) (hhsize : h.size = dh + 1) (hh : h = f + b * g) : poly J f g = scale (SubresultantMinor.sign ((df - J) * (dg - J)) * g.leadingCoeff ^ (df - dh)) (poly J g h)

Polynomial form of the Brown--Traub transformation at or below the degree of H.

theorem Hex.DensePoly.Subresultant.poly_descent {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g h : DensePoly R) {c : R} (hc : c ≠ 0) (hg : g ≠ 0) (hh : h ≠ 0) (hgf : g.size ≤ f.size) (hp : (f.pseudoDivMod g).snd = scale c h) (J : Nat) (hJ : J < h.size) : scale (g.leadingCoeff ^ ((f.size - g.size + 1) * (g.size - 1 - J))) (poly J f g) = scale (SubresultantMinor.sign ((f.size - 1 - J) * (g.size - 1 - J)) * g.leadingCoeff ^ (f.size - h.size) * c ^ (g.size - 1 - J)) (poly J g h)

Transport a generalized subresultant family across one scaled pseudo-remainder step. The identity stays cross-multiplied, so every scalar remains in the base ring even across defective degree drops.

theorem Hex.DensePoly.Subresultant.poly_brownTraub_rightDegree {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (df dg db dh : Nat) (f g b h : DensePoly R) (hdh : dh < dg) (hdeg : df = db + dg) (hf : f.size = df + 1) (hg : g.size = dg + 1) (hb : b.size ≤ db + 1) (hhsize : h.size = dh + 1) (hh : h = f + b * g) : poly dh f g = scale (SubresultantMinor.sign ((df - dh) * (dg - dh)) * g.leadingCoeff ^ (df - dh) * h.leadingCoeff ^ (dg - dh - 1)) h

Endpoint form of Brown--Traub equation (12), including both leading coefficient powers.

theorem Hex.DensePoly.Subresultant.divScalar_brownTraub {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (df dg db dh : Nat) (f g b h : DensePoly R) (hdh : dh < dg) (hdeg : df = db + dg) (hf : f.size = df + 1) (hg : g.size = dg + 1) (hb : b.size ≤ db + 1) (hhsize : h.size = dh + 1) (hh : h = f + b * g) (h1 : 1 ≠ 0) : (poly dh f g).divScalar (SubresultantMinor.sign ((df - dh) * (dg - dh)) * g.leadingCoeff ^ (df - dh) * h.leadingCoeff ^ (dg - dh - 1)) = h

The endpoint factorization makes its scalar quotient coefficientwise exact in every lawful exact-division domain.

theorem Hex.DensePoly.Subresultant.coeffMinor_zero_of_prem_zero {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g : DensePoly R) (hg : g ≠ 0) (hgf : g.size ≤ f.size) (hgBig : 2 ≤ g.size) (hp : (f.pseudoDivMod g).snd = 0) : coeffMinor 0 0 f g = 0

If an ordered pseudo-division terminates at a nonconstant divisor, the zeroth generalized subresultant vanishes.