24.4. Integral proof and coefficient embeddings🔗

Brown--Traub exactness is proved directly in the input coefficient ring. The recursive invariant keeps every leading-coefficient and Brown-scale factor cross-multiplied, then cancels only factors already proved nonzero. This gives the scalar and coefficientwise reconstruction equations required by the Brown recurrence without changing coefficient types.

The Mathlib-free fraction field remains available as general proof infrastructure. Its embedding is injective, commutes with ordered pseudo-division, and supports pulling exact quotients back to the coefficient ring, but the Brown recurrence does not depend on that detour.

def

Hex.Fraction.ofCoeff.{u} {R : Type u} [Lean.Grind.CommRing R] [Div R]
  [Hex.ExactDivLaws R] [Hex.Fraction.NonzeroOne R] (a : R) :
  Hex.Fraction R
Hex.Fraction.ofCoeff.{u} {R : Type u}
  [Lean.Grind.CommRing R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (a : R) :
  Hex.Fraction R

Embed a coefficient as a fraction with denominator one.

theorem

Hex.Fraction.ofCoeff_injective.{u} {R : Type u} [Lean.Grind.CommRing R]
  [Div R] [Hex.ExactDivLaws R] [Hex.Fraction.NonzeroOne R] {a b : R}
  (h : Hex.Fraction.ofCoeff a = Hex.Fraction.ofCoeff b) : a = b
Hex.Fraction.ofCoeff_injective.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [Div R] [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] {a b : R}
  (h :
    Hex.Fraction.ofCoeff a =
      Hex.Fraction.ofCoeff b) :
  a = b

The coefficient embedding is injective.

def

Hex.DensePoly.Fraction.map.{u} {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (p : Hex.DensePoly R) :
  Hex.DensePoly (Hex.Fraction R)
Hex.DensePoly.Fraction.map.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R]
  (p : Hex.DensePoly R) :
  Hex.DensePoly (Hex.Fraction R)

Embed every coefficient of a dense polynomial into the fraction field.

theorem

Hex.Fraction.div_pullback.{u} {R : Type u} [Lean.Grind.CommRing R]
  [Div R] [Hex.ExactDivLaws R] [Hex.Fraction.NonzeroOne R]
  [DecidableEq R] {a b c : R} (hb : b ≠ 0)
  (h :
    Hex.Fraction.ofCoeff c =
      Hex.Fraction.ofCoeff a / Hex.Fraction.ofCoeff b) :
  a / b = c
Hex.Fraction.div_pullback.{u} {R : Type u}
  [Lean.Grind.CommRing R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R]
  [DecidableEq R] {a b c : R} (hb : b ≠ 0)
  (h :
    Hex.Fraction.ofCoeff c =
      Hex.Fraction.ofCoeff a /
        Hex.Fraction.ofCoeff b) :
  a / b = c

Pull an exact scalar quotient back through the coefficient embedding.

The hypothesis that the fraction quotient lies in the image is the integrality fact supplied by generalized subresultants.

theorem

Hex.Fraction.divExp_exact.{u} {R : Type u} [Lean.Grind.CommRing R]
  [Div R] [Hex.ExactDivLaws R] [Hex.Fraction.NonzeroOne R]
  [DecidableEq R] (x y : R) (n : ℕ) (hden : Hex.powNat y (n - 1) ≠ 0)
  (h :
    ∃ c,
      Hex.Fraction.ofCoeff c =
        Hex.Fraction.ofCoeff (Hex.powNat x n) /
          Hex.Fraction.ofCoeff (Hex.powNat y (n - 1))) :
  Hex.powNat x n = Hex.powNat y (n - 1) * Hex.divExp x y n
Hex.Fraction.divExp_exact.{u} {R : Type u}
  [Lean.Grind.CommRing R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R]
  [DecidableEq R] (x y : R) (n : ℕ)
  (hden : Hex.powNat y (n - 1) ≠ 0)
  (h :
    ∃ c,
      Hex.Fraction.ofCoeff c =
        Hex.Fraction.ofCoeff
            (Hex.powNat x n) /
          Hex.Fraction.ofCoeff
            (Hex.powNat y (n - 1))) :
  Hex.powNat x n =
    Hex.powNat y (n - 1) *
      Hex.divExp x y n

A Brown scalar quotient in the embedding image satisfies the exact scale recurrence used by BrownLaw.

theorem

Hex.DensePoly.Fraction.map_pseudoDivMod.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (f g : Hex.DensePoly R) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  (Hex.DensePoly.Fraction.map f).pseudoDivMod
      (Hex.DensePoly.Fraction.map g) =
    (Hex.DensePoly.Fraction.map (f.pseudoDivMod g).1,
      Hex.DensePoly.Fraction.map (f.pseudoDivMod g).2)
Hex.DensePoly.Fraction.map_pseudoDivMod.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R]
  (f g : Hex.DensePoly R) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  (Hex.DensePoly.Fraction.map
          f).pseudoDivMod
      (Hex.DensePoly.Fraction.map g) =
    (Hex.DensePoly.Fraction.map
        (f.pseudoDivMod g).1,
      Hex.DensePoly.Fraction.map
        (f.pseudoDivMod g).2)

Pseudo-division commutes with the fraction-field embedding on an ordered nonzero input pair.

theorem

Hex.DensePoly.Fraction.divScalar_pullback.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (p q : Hex.DensePoly R) {b : R}
  (hb : b ≠ 0)
  (h :
    Hex.DensePoly.Fraction.map q =
      (Hex.DensePoly.Fraction.map p).divScalar
        (Hex.Fraction.ofCoeff b)) :
  p.divScalar b = q
Hex.DensePoly.Fraction.divScalar_pullback.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R]
  (p q : Hex.DensePoly R) {b : R}
  (hb : b ≠ 0)
  (h :
    Hex.DensePoly.Fraction.map q =
      (Hex.DensePoly.Fraction.map
            p).divScalar
        (Hex.Fraction.ofCoeff b)) :
  p.divScalar b = q

Pull coefficientwise exact scalar division back from the fraction field.

The image hypothesis is the integrality certificate later supplied by a generalized subresultant minor.

theorem

Hex.DensePoly.Fraction.divScalar_exact.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (p : Hex.DensePoly R) {b : R} (hb : b ≠ 0)
  (h :
    ∀ (n : ℕ),
      ∃ c,
        Hex.Fraction.ofCoeff c =
          Hex.Fraction.ofCoeff (p.coeff n) / Hex.Fraction.ofCoeff b) :
  p = Hex.DensePoly.scale b (p.divScalar b)
Hex.DensePoly.Fraction.divScalar_exact.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R]
  (p : Hex.DensePoly R) {b : R}
  (hb : b ≠ 0)
  (h :
    ∀ (n : ℕ),
      ∃ c,
        Hex.Fraction.ofCoeff c =
          Hex.Fraction.ofCoeff
              (p.coeff n) /
            Hex.Fraction.ofCoeff b) :
  p =
    Hex.DensePoly.scale b (p.divScalar b)

Coefficientwise integrality in the fraction field proves that executable scalar division reconstructs the original polynomial.

The generalized subresultants are coefficient-indexed scalar determinants local to HexResultant; they do not introduce a dependency on the matrix libraries. Their explicit-degree core makes preservation under the fraction embedding type-stable. The Brown--Traub identities identify the later scalar and polynomial quotients with these mapped subresultants, whose coefficients then have base-ring image witnesses.

def

Hex.DensePoly.Subresultant.coeffMinor.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (J l : ℕ)
  (f g : Hex.DensePoly R) : R
Hex.DensePoly.Subresultant.coeffMinor.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R]
  (J l : ℕ) (f g : Hex.DensePoly R) : R

One scalar coefficient minor of the J-th generalized subresultant.

def

Hex.DensePoly.Subresultant.poly.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (J : ℕ)
  (f g : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.Subresultant.poly.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] (J : ℕ)
  (f g : Hex.DensePoly R) :
  Hex.DensePoly R

Generalized Sylvester subresultant, assembled coefficientwise from scalar minors. Its degree is at most J.

theorem

Hex.DensePoly.Subresultant.poly_size_le.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (J : ℕ)
  (f g : Hex.DensePoly R) :
  (Hex.DensePoly.Subresultant.poly J f g).size ≤ J + 1
Hex.DensePoly.Subresultant.poly_size_le.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] (J : ℕ)
  (f g : Hex.DensePoly R) :
  (Hex.DensePoly.Subresultant.poly J f
        g).size ≤
    J + 1

The coefficient construction stores no terms above subresultant index J.

The local Laplace determinant supplies column multilinearity, arbitrary alternation and column updates, and the parity law for adjacent-transposition sequences without importing hex-matrix or hex-determinant. In particular, scaling either input polynomial scales the generalized subresultant by one scalar for each column in that input's Sylvester block. A consecutive-block rotation then exchanges those blocks, contributing one sign for every crossed pair of columns and yielding the generalized-subresultant input-swap law.

The column-operation form of Brown--Traub equation (18) is the next transformation. Starting from the swapped G, F matrix, the specialized unit upper-triangular update adds multiplier-weighted G columns into the later F columns. When H = F + B * G and the formal degrees satisfy deg F = deg B + deg G, the coefficient convolution replaces every F column by the matching H column. The target is the ordinary generalized Sylvester matrix for G, H, with F's formal degree retained explicitly even when H drops in degree. The determinant is unchanged by these additions, so the only factor is the block-swap sign.

Collapsing the retained formal degree then exposes one sparse first row per removed degree. Each expansion contributes lc(G), while the final edge subresultant is lc(H)^(deg G - deg H - 1) H. Together these identities give the full Brown--Traub factorization, and a nonzero factor can be divided out coefficientwise by the executable exact-division operation.

theorem

Hex.SubresultantMinor.det_setCol_add.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} (M : Hex.SubresultantMinor.Square R n)
  (dst : Fin n) (v w : Fin n → R) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.setCol M dst fun i => v i + w i) =
    Hex.SubresultantMinor.det (Hex.SubresultantMinor.setCol M dst v) +
      Hex.SubresultantMinor.det (Hex.SubresultantMinor.setCol M dst w)
Hex.SubresultantMinor.det_setCol_add.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M : Hex.SubresultantMinor.Square R n)
  (dst : Fin n) (v w : Fin n → R) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.setCol M dst
        fun i => v i + w i) =
    Hex.SubresultantMinor.det
        (Hex.SubresultantMinor.setCol M
          dst v) +
      Hex.SubresultantMinor.det
        (Hex.SubresultantMinor.setCol M
          dst w)

The local Laplace determinant is additive in any replaced column.

theorem

Hex.SubresultantMinor.det_swapAdjacent.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (M : Hex.SubresultantMinor.Square R (n + 1)) (left : Fin n) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.swapAdjacent M left) =
    0 - Hex.SubresultantMinor.det M
Hex.SubresultantMinor.det_swapAdjacent.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M :
    Hex.SubresultantMinor.Square R
      (n + 1))
  (left : Fin n) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.swapAdjacent
        M left) =
    0 - Hex.SubresultantMinor.det M

Swapping two adjacent columns negates the local determinant.

theorem

Hex.SubresultantMinor.det_applySwaps.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (M : Hex.SubresultantMinor.Square R (n + 1)) (swaps : List (Fin n)) :
  Hex.SubresultantMinor.det (Hex.SubresultantMinor.applySwaps M swaps) =
    Hex.SubresultantMinor.sign swaps.length *
      Hex.SubresultantMinor.det M
Hex.SubresultantMinor.det_applySwaps.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M :
    Hex.SubresultantMinor.Square R
      (n + 1))
  (swaps : List (Fin n)) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.applySwaps M
        swaps) =
    Hex.SubresultantMinor.sign
        swaps.length *
      Hex.SubresultantMinor.det M

A sequence of adjacent column transpositions multiplies the local determinant by its parity sign.

def

Hex.SubresultantMinor.rotateBlocks.{u} {R : Type u} {n : ℕ}
  (M : Hex.SubresultantMinor.Square R n) (start left right : ℕ) :
  start + left + right ≤ n → Hex.SubresultantMinor.Square R n
Hex.SubresultantMinor.rotateBlocks.{u}
  {R : Type u} {n : ℕ}
  (M : Hex.SubresultantMinor.Square R n)
  (start left right : ℕ) :
  start + left + right ≤ n →
    Hex.SubresultantMinor.Square R n

Rotate consecutive blocks of lengths left and right beginning at start, changing [A, B] to [B, A].

theorem

Hex.SubresultantMinor.det_rotateBlocks.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} (M : Hex.SubresultantMinor.Square R n)
  (start left right : ℕ) (h : start + left + right ≤ n) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.rotateBlocks M start left right h) =
    Hex.SubresultantMinor.sign (left * right) *
      Hex.SubresultantMinor.det M
Hex.SubresultantMinor.det_rotateBlocks.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M : Hex.SubresultantMinor.Square R n)
  (start left right : ℕ)
  (h : start + left + right ≤ n) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.rotateBlocks
        M start left right h) =
    Hex.SubresultantMinor.sign
        (left * right) *
      Hex.SubresultantMinor.det M

Rotating consecutive blocks contributes one adjacent swap for each pair of columns drawn from opposite blocks.

theorem

Hex.SubresultantMinor.det_eq_zero_of_col_eq.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} (M : Hex.SubresultantMinor.Square R n)
  (a b : Fin n) (hab : a ≠ b) (hcol : ∀ (i : Fin n), M i a = M i b) :
  Hex.SubresultantMinor.det M = 0
Hex.SubresultantMinor.det_eq_zero_of_col_eq.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M : Hex.SubresultantMinor.Square R n)
  (a b : Fin n) (hab : a ≠ b)
  (hcol : ∀ (i : Fin n), M i a = M i b) :
  Hex.SubresultantMinor.det M = 0

The local determinant vanishes when any two distinct columns agree.

theorem

Hex.SubresultantMinor.det_addCol.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} (M : Hex.SubresultantMinor.Square R n)
  (src dst : Fin n) (c : R) (h : src ≠ dst) :
  Hex.SubresultantMinor.det (Hex.SubresultantMinor.addCol M src dst c) =
    Hex.SubresultantMinor.det M
Hex.SubresultantMinor.det_addCol.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M : Hex.SubresultantMinor.Square R n)
  (src dst : Fin n) (c : R)
  (h : src ≠ dst) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.addCol M src
        dst c) =
    Hex.SubresultantMinor.det M

Adding a scalar multiple of one column to a distinct column preserves the local determinant.

theorem

Hex.SubresultantMinor.det_scaleRange.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} (M : Hex.SubresultantMinor.Square R n)
  (start count : ℕ) (c : R) (hbound : start + count ≤ n) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.scaleRange M start count c) =
    c ^ count * Hex.SubresultantMinor.det M
Hex.SubresultantMinor.det_scaleRange.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M : Hex.SubresultantMinor.Square R n)
  (start count : ℕ) (c : R)
  (hbound : start + count ≤ n) :
  Hex.SubresultantMinor.det
      (Hex.SubresultantMinor.scaleRange M
        start count c) =
    c ^ count *
      Hex.SubresultantMinor.det M

Scaling count consecutive columns scales the determinant by c ^ count.

theorem

Hex.SubresultantMinor.det_firstRow.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (M : Hex.SubresultantMinor.Square R (n + 1))
  (hzero : ∀ (j : Fin (n + 1)), 0 < ↑j → M ⟨0, ⋯⟩ j = 0) :
  Hex.SubresultantMinor.det M =
    M ⟨0, ⋯⟩ ⟨0, ⋯⟩ *
      Hex.SubresultantMinor.det
        (Hex.SubresultantMinor.deleteFirst M ⟨0, ⋯⟩)
Hex.SubresultantMinor.det_firstRow.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : ℕ}
  (M :
    Hex.SubresultantMinor.Square R
      (n + 1))
  (hzero :
    ∀ (j : Fin (n + 1)),
      0 < ↑j → M ⟨0, ⋯⟩ j = 0) :
  Hex.SubresultantMinor.det M =
    M ⟨0, ⋯⟩ ⟨0, ⋯⟩ *
      Hex.SubresultantMinor.det
        (Hex.SubresultantMinor.deleteFirst
          M ⟨0, ⋯⟩)

If the first row is supported only in its first column, the local determinant expands to that entry times the remaining first minor.

theorem

Hex.DensePoly.Subresultant.poly_scale_left.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  {c : R} (hc : c ≠ 0) (J : ℕ) (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J (Hex.DensePoly.scale c f) g =
    Hex.DensePoly.scale
      (c ^ (Hex.DensePoly.Subresultant.formalDegree g - J))
      (Hex.DensePoly.Subresultant.poly J f g)
Hex.DensePoly.Subresultant.poly_scale_left.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R] {c : R}
  (hc : c ≠ 0) (J : ℕ)
  (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J
      (Hex.DensePoly.scale c f) g =
    Hex.DensePoly.scale
      (c ^
        (Hex.DensePoly.Subresultant.formalDegree
            g -
          J))
      (Hex.DensePoly.Subresultant.poly J f
        g)

Generalized subresultants are homogeneous in the left polynomial.

theorem

Hex.DensePoly.Subresultant.poly_scale_right.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  {c : R} (hc : c ≠ 0) (J : ℕ) (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J f (Hex.DensePoly.scale c g) =
    Hex.DensePoly.scale
      (c ^ (Hex.DensePoly.Subresultant.formalDegree f - J))
      (Hex.DensePoly.Subresultant.poly J f g)
Hex.DensePoly.Subresultant.poly_scale_right.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R] {c : R}
  (hc : c ≠ 0) (J : ℕ)
  (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J f
      (Hex.DensePoly.scale c g) =
    Hex.DensePoly.scale
      (c ^
        (Hex.DensePoly.Subresultant.formalDegree
            f -
          J))
      (Hex.DensePoly.Subresultant.poly J f
        g)

Generalized subresultants are homogeneous in the right polynomial.

theorem

Hex.DensePoly.Subresultant.poly_swap.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (J : ℕ)
  (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J f g =
    Hex.DensePoly.scale
      (Hex.SubresultantMinor.sign
        ((Hex.DensePoly.Subresultant.formalDegree f - J) *
          (Hex.DensePoly.Subresultant.formalDegree g - J)))
      (Hex.DensePoly.Subresultant.poly J g f)
Hex.DensePoly.Subresultant.poly_swap.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (J : ℕ)
  (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J f g =
    Hex.DensePoly.scale
      (Hex.SubresultantMinor.sign
        ((Hex.DensePoly.Subresultant.formalDegree
              f -
            J) *
          (Hex.DensePoly.Subresultant.formalDegree
              g -
            J)))
      (Hex.DensePoly.Subresultant.poly J g
        f)

Generalized Sylvester subresultants obey the standard input-swap sign law.

theorem

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

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

theorem

Hex.DensePoly.Subresultant.productCols_addMul.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (df dg db J l : ℕ)
  (f g b h : Hex.DensePoly R) (hJ : J < dg) (hdeg : df = db + dg)
  (hb : b.size ≤ db + 1) (hh : h = f + b * g) :
  Hex.SubresultantMinor.productCols
      (Hex.DensePoly.Subresultant.coeffMatrixAt dg df J l g f) (df - J)
      db b (dg - J) ⋯ ⋯ =
    Hex.DensePoly.Subresultant.coeffMatrixAt dg df J l g h
Hex.DensePoly.Subresultant.productCols_addMul.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (df dg db J l : ℕ)
  (f g b h : Hex.DensePoly R)
  (hJ : J < dg) (hdeg : df = db + dg)
  (hb : b.size ≤ db + 1)
  (hh : h = f + b * g) :
  Hex.SubresultantMinor.productCols
      (Hex.DensePoly.Subresultant.coeffMatrixAt
        dg df J l g f)
      (df - J) db b (dg - J) ⋯ ⋯ =
    Hex.DensePoly.Subresultant.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (df dg db J l : ℕ)
  (f g b h : Hex.DensePoly R) (hJ : J < dg) (hdeg : df = db + dg)
  (hb : b.size ≤ db + 1) (hh : h = f + b * g) :
  Hex.SubresultantMinor.det
      (Hex.DensePoly.Subresultant.coeffMatrixAt dg df J l g h) =
    Hex.SubresultantMinor.det
      (Hex.DensePoly.Subresultant.coeffMatrixAt dg df J l g f)
Hex.DensePoly.Subresultant.det_addMul.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (df dg db J l : ℕ)
  (f g b h : Hex.DensePoly R)
  (hJ : J < dg) (hdeg : df = db + dg)
  (hb : b.size ≤ db + 1)
  (hh : h = f + b * g) :
  Hex.SubresultantMinor.det
      (Hex.DensePoly.Subresultant.coeffMatrixAt
        dg df J l g h) =
    Hex.SubresultantMinor.det
      (Hex.DensePoly.Subresultant.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (df dg db J l : ℕ)
  (f g b h : Hex.DensePoly R) (hJ : J < dg) (hdeg : df = db + dg)
  (hb : b.size ≤ db + 1) (hh : h = f + b * g) :
  Hex.DensePoly.Subresultant.coeffMinorAt df dg J l f g =
    Hex.SubresultantMinor.sign ((df - J) * (dg - J)) *
      Hex.DensePoly.Subresultant.coeffMinorAt dg df J l g h
Hex.DensePoly.Subresultant.coeffMinorAt_addMul.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (df dg db J l : ℕ)
  (f g b h : Hex.DensePoly R)
  (hJ : J < dg) (hdeg : df = db + dg)
  (hb : b.size ≤ db + 1)
  (hh : h = f + b * g) :
  Hex.DensePoly.Subresultant.coeffMinorAt
      df dg J l f g =
    Hex.SubresultantMinor.sign
        ((df - J) * (dg - J)) *
      Hex.DensePoly.Subresultant.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (dg dh J l : ℕ)
  (g h : Hex.DensePoly R) (hpos : 0 < dg - J + (dh - J)) (hJh : J ≤ dh)
  (hg : g.size = dg + 1) (hh : h.size ≤ dh + 1) :
  Hex.DensePoly.Subresultant.coeffMinorAt dg (dh + 1) J l g h =
    g.leadingCoeff *
      Hex.DensePoly.Subresultant.coeffMinorAt dg dh J l g h
Hex.DensePoly.Subresultant.coeffMinorAt_succRight.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (dg dh J l : ℕ)
  (g h : Hex.DensePoly R)
  (hpos : 0 < dg - J + (dh - J))
  (hJh : J ≤ dh) (hg : g.size = dg + 1)
  (hh : h.size ≤ dh + 1) :
  Hex.DensePoly.Subresultant.coeffMinorAt
      dg (dh + 1) J l g h =
    g.leadingCoeff *
      Hex.DensePoly.Subresultant.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (dg dh J l extra : ℕ)
  (g h : Hex.DensePoly R) (hpos : 0 < dg - J + (dh - J)) (hJh : J ≤ dh)
  (hg : g.size = dg + 1) (hh : h.size ≤ dh + 1) :
  Hex.DensePoly.Subresultant.coeffMinorAt dg (dh + extra) J l g h =
    g.leadingCoeff ^ extra *
      Hex.DensePoly.Subresultant.coeffMinorAt dg dh J l g h
Hex.DensePoly.Subresultant.coeffMinorAt_raiseRight.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (dg dh J l extra : ℕ)
  (g h : Hex.DensePoly R)
  (hpos : 0 < dg - J + (dh - J))
  (hJh : J ≤ dh) (hg : g.size = dg + 1)
  (hh : h.size ≤ dh + 1) :
  Hex.DensePoly.Subresultant.coeffMinorAt
      dg (dh + extra) J l g h =
    g.leadingCoeff ^ extra *
      Hex.DensePoly.Subresultant.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_rightDegree.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (dg dh l : ℕ)
  (g h : Hex.DensePoly R) (hdh : dh < dg) (hh : h.size = dh + 1) :
  Hex.DensePoly.Subresultant.coeffMinorAt dg dh dh l g h =
    h.leadingCoeff ^ (dg - dh - 1) * h.coeff l
Hex.DensePoly.Subresultant.coeffMinorAt_rightDegree.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (dg dh l : ℕ)
  (g h : Hex.DensePoly R) (hdh : dh < dg)
  (hh : h.size = dh + 1) :
  Hex.DensePoly.Subresultant.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (df dg db dh J l : ℕ)
  (f g b h : Hex.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) :
  Hex.DensePoly.Subresultant.coeffMinorAt df dg J l f g =
    Hex.SubresultantMinor.sign ((df - J) * (dg - J)) *
      (g.leadingCoeff ^ (df - dh) *
        Hex.DensePoly.Subresultant.coeffMinorAt dg dh J l g h)
Hex.DensePoly.Subresultant.coeffMinorAt_brownTraub.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (df dg db dh J l : ℕ)
  (f g b h : Hex.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) :
  Hex.DensePoly.Subresultant.coeffMinorAt
      df dg J l f g =
    Hex.SubresultantMinor.sign
        ((df - J) * (dg - J)) *
      (g.leadingCoeff ^ (df - dh) *
        Hex.DensePoly.Subresultant.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (dg dh : ℕ)
  (g h : Hex.DensePoly R) (hdh : dh < dg) (hg : g.size = dg + 1)
  (hh : h.size = dh + 1) :
  Hex.DensePoly.Subresultant.poly dh g h =
    Hex.DensePoly.scale (h.leadingCoeff ^ (dg - dh - 1)) h
Hex.DensePoly.Subresultant.poly_rightDegree.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (dg dh : ℕ)
  (g h : Hex.DensePoly R) (hdh : dh < dg)
  (hg : g.size = dg + 1)
  (hh : h.size = dh + 1) :
  Hex.DensePoly.Subresultant.poly dh g h =
    Hex.DensePoly.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (df dg db dh J : ℕ)
  (f g b h : Hex.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) :
  Hex.DensePoly.Subresultant.poly J f g =
    Hex.DensePoly.scale
      (Hex.SubresultantMinor.sign ((df - J) * (dg - J)) *
        g.leadingCoeff ^ (df - dh))
      (Hex.DensePoly.Subresultant.poly J g h)
Hex.DensePoly.Subresultant.poly_brownTraub.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (df dg db dh J : ℕ)
  (f g b h : Hex.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) :
  Hex.DensePoly.Subresultant.poly J f g =
    Hex.DensePoly.scale
      (Hex.SubresultantMinor.sign
          ((df - J) * (dg - J)) *
        g.leadingCoeff ^ (df - dh))
      (Hex.DensePoly.Subresultant.poly J g
        h)

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

theorem

Hex.DensePoly.Subresultant.poly_brownTraub_rightDegree.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] (df dg db dh : ℕ)
  (f g b h : Hex.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) :
  Hex.DensePoly.Subresultant.poly dh f g =
    Hex.DensePoly.scale
      (Hex.SubresultantMinor.sign ((df - dh) * (dg - dh)) *
          g.leadingCoeff ^ (df - dh) *
        h.leadingCoeff ^ (dg - dh - 1))
      h
Hex.DensePoly.Subresultant.poly_brownTraub_rightDegree.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] (df dg db dh : ℕ)
  (f g b h : Hex.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) :
  Hex.DensePoly.Subresultant.poly dh f g =
    Hex.DensePoly.scale
      (Hex.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.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  (df dg db dh : ℕ) (f g b h : Hex.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) :
  (Hex.DensePoly.Subresultant.poly dh f g).divScalar
      (Hex.SubresultantMinor.sign ((df - dh) * (dg - dh)) *
          g.leadingCoeff ^ (df - dh) *
        h.leadingCoeff ^ (dg - dh - 1)) =
    h
Hex.DensePoly.Subresultant.divScalar_brownTraub.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R] (df dg db dh : ℕ)
  (f g b h : Hex.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) :
  (Hex.DensePoly.Subresultant.poly dh f
          g).divScalar
      (Hex.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.

The pseudo-remainder specialization covers defective degree drops as well as regular steps. It identifies the subresultant immediately below the divisor degree, transports every lower subresultant across the step, and feeds the cross-multiplied family invariant used by the recursive proof.

theorem

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

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

def

Hex.DensePoly.BrownLaw.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (prev curr : Hex.DensePoly R)
  (hPrev : R) : ℕ → Prop
Hex.DensePoly.BrownLaw.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (prev curr : Hex.DensePoly R)
  (hPrev : R) : ℕ → Prop

The exactness and nonzero obligations for every reachable Brown worker state. A valid state must terminate naturally before its fuel reaches zero; the adjacent polynomials have strictly decreasing size, the current and successor scales are nonzero, both scalar divisions reconstruct their numerators, the Brown divisor and quotient are nonzero, and the successor is valid.

theorem

Hex.DensePoly.subresultantOrdered_brownLaw.{u} {S : Type u}
  [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) (hg : g ≠ 0) (hgf : g.size ≤ f.size) :
  have delta := f.size - g.size;
  have h₂ := Hex.powNat g.leadingCoeff delta;
  have p := (f.pseudoDivMod g).2;
  if p.isZero = true then h₂ ≠ 0
  else
    have g₃ :=
      Hex.DensePoly.scaleImpl (Hex.DensePoly.negOnePow (delta + 1)) p;
    g₃ ≠ 0 ∧ g.BrownLaw g₃ h₂ (g.size + 1)
Hex.DensePoly.subresultantOrdered_brownLaw.{u}
  {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S] [Div S]
  [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  have delta := f.size - g.size;
  have h₂ :=
    Hex.powNat g.leadingCoeff delta;
  have p := (f.pseudoDivMod g).2;
  if p.isZero = true then h₂ ≠ 0
  else
    have g₃ :=
      Hex.DensePoly.scaleImpl
        (Hex.DensePoly.negOnePow
          (delta + 1))
        p;
    g₃ ≠ 0 ∧ g.BrownLaw g₃ h₂ (g.size + 1)

Ordered nonzero inputs establish every nonzero-denominator and exactness obligation recorded by BrownLaw, including the unreachability of the junk zero-quotient branch.

theorem

Hex.DensePoly.Subresultant.Fraction.poly_map.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (J : ℕ) (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J (Hex.DensePoly.Fraction.map f)
      (Hex.DensePoly.Fraction.map g) =
    Hex.DensePoly.Fraction.map (Hex.DensePoly.Subresultant.poly J f g)
Hex.DensePoly.Subresultant.Fraction.poly_map.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (J : ℕ)
  (f g : Hex.DensePoly R) :
  Hex.DensePoly.Subresultant.poly J
      (Hex.DensePoly.Fraction.map f)
      (Hex.DensePoly.Fraction.map g) =
    Hex.DensePoly.Fraction.map
      (Hex.DensePoly.Subresultant.poly J f
        g)

Generalized Sylvester subresultants commute with the polynomial coefficient embedding. In particular, every coefficient of the fraction construction has an explicit base-ring image witness.

theorem

Hex.DensePoly.Subresultant.Fraction.exists_coeff.{u} {R : Type u}
  [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (J : ℕ) (f g : Hex.DensePoly R) (l : ℕ) :
  ∃ c,
    Hex.Fraction.ofCoeff c =
      (Hex.DensePoly.Subresultant.poly J (Hex.DensePoly.Fraction.map f)
            (Hex.DensePoly.Fraction.map g)).coeff
        l
Hex.DensePoly.Subresultant.Fraction.exists_coeff.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  [Hex.Fraction.NonzeroOne R] (J : ℕ)
  (f g : Hex.DensePoly R) (l : ℕ) :
  ∃ c,
    Hex.Fraction.ofCoeff c =
      (Hex.DensePoly.Subresultant.poly J
            (Hex.DensePoly.Fraction.map f)
            (Hex.DensePoly.Fraction.map
              g)).coeff
        l

Coefficients of mapped generalized subresultants lie in the coefficient embedding image.