21.1. HexResultant: subresultants and discriminants🔗

21.1.1. Introduction🔗

HexResultant computes polynomial resultants and discriminants without constructing a Sylvester matrix. Its Brown subresultant pseudo-remainder sequence stays in the coefficient ring and uses exact division only at the points where the recurrence proves divisibility. This matters for the tower algorithms later in the manual: their coefficient rings are executable number-field presentations, not Mathlib fields.

The computational library is Mathlib-free. HexResultantMathlib states the correspondence between the final executable value and Polynomial.resultant, including specialization and discriminant conventions.

Exact division is governed by the algebraic law ExactDivLaws, which the correctness proofs discharge rather than assuming laws for the total / operation. The executable carries no runtime divisibility check; the algorithm only invokes division at factors whose divisibility the Brown recurrence has established:

type class

Hex.ExactDivLaws.{u} (R : Type u) [Zero R] [Mul R] [Div R] : Prop
Hex.ExactDivLaws.{u} (R : Type u) [Zero R]
  [Mul R] [Div R] : Prop

A quotient operation is exact when multiplication by every nonzero right factor can be undone by division by that factor.

Instance Constructor

Hex.ExactDivLaws.mk.{u}

Methods

mul_div_cancel_right : ∀ (a b : R), b ≠ 0 → a * b / b = a

Right multiplication followed by division by a nonzero factor cancels.

21.1.2. The executable API🔗

The public chain records its normalized inputs, every nonzero remainder, and the terminal principal-subresultant scalar. The scalar is separate because a defective degree drop can change the exact resultant without changing the last nonzero polynomial.

structure

Hex.PRSResult.{u} (R : Type u) [Zero R] [DecidableEq R] : Type u
Hex.PRSResult.{u} (R : Type u) [Zero R]
  [DecidableEq R] : Type u

Executable result of a degree-ordered Brown PRS run.

scale belongs to the ordered chain. In particular, subresultantRun does not record whether it swapped its arguments, so this structure alone is not a caller-order-sensitive resultant; use resultant for that value.

Constructor

Hex.PRSResult.mk.{u}

Fields

chain : Array (Hex.DensePoly R)

Brown's nonzero G₁, …, Gₖ, excluding the generated terminal zero.

scale : R

Corrected terminal principal-subresultant scalar hₖ.

def

Hex.DensePoly.subresultantChain.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) : Array (Hex.DensePoly R)
Hex.DensePoly.subresultantChain.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) :
  Array (Hex.DensePoly R)

Brown's nonzero subresultant pseudo-remainder sequence.

21.1.3. Certified pseudo-division algebra🔗

The coefficient recurrence is characterized independently of its array implementation: reconstruction and a remainder smaller than the divisor determine the quotient/remainder pair uniquely. Nonzero scaling of either input then follows from that characterization.

theorem

Hex.DensePoly.pseudoDivMod_unique.{u} {S : Type u}
  [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [Hex.ExactDivLaws S]
  (f g q r : Hex.DensePoly S) (hg : g ≠ 0) (hgf : g.size ≤ f.size)
  (hrec :
    Hex.DensePoly.scale (g.leadingCoeff ^ (f.size - g.size + 1)) f =
      q * g + r)
  (hr : r.size < g.size) : f.pseudoDivMod g = (q, r)
Hex.DensePoly.pseudoDivMod_unique.{u}
  {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S] [Div S]
  [Hex.ExactDivLaws S]
  (f g q r : Hex.DensePoly S) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size)
  (hrec :
    Hex.DensePoly.scale
        (g.leadingCoeff ^
          (f.size - g.size + 1))
        f =
      q * g + r)
  (hr : r.size < g.size) :
  f.pseudoDivMod g = (q, r)

Reconstruction and the strict remainder bound uniquely characterize pseudoDivMod on an ordered nonzero input pair.

theorem

Hex.DensePoly.pseudoDivMod_scale_left.{u} {S : Type u}
  [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) {a : S} (ha : a ≠ 0) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  (Hex.DensePoly.scale a f).pseudoDivMod g =
    (Hex.DensePoly.scale a (f.pseudoDivMod g).1,
      Hex.DensePoly.scale a (f.pseudoDivMod g).2)
Hex.DensePoly.pseudoDivMod_scale_left.{u}
  {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S] [Div S]
  [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) {a : S}
  (ha : a ≠ 0) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  (Hex.DensePoly.scale a f).pseudoDivMod
      g =
    (Hex.DensePoly.scale a
        (f.pseudoDivMod g).1,
      Hex.DensePoly.scale a
        (f.pseudoDivMod g).2)

Scaling the dividend scales both pseudo-division outputs.

theorem

Hex.DensePoly.pseudoDivMod_scale_right.{u} {S : Type u}
  [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) {a : S} (ha : a ≠ 0) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  have d := f.size - g.size + 1;
  f.pseudoDivMod (Hex.DensePoly.scale a g) =
    (Hex.DensePoly.scale (a ^ (d - 1)) (f.pseudoDivMod g).1,
      Hex.DensePoly.scale (a ^ d) (f.pseudoDivMod g).2)
Hex.DensePoly.pseudoDivMod_scale_right.{u}
  {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S] [Div S]
  [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) {a : S}
  (ha : a ≠ 0) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  have d := f.size - g.size + 1;
  f.pseudoDivMod
      (Hex.DensePoly.scale a g) =
    (Hex.DensePoly.scale (a ^ (d - 1))
        (f.pseudoDivMod g).1,
      Hex.DensePoly.scale (a ^ d)
        (f.pseudoDivMod g).2)

Scaling the divisor by a scales the pseudo-quotient by a^(d-1) and the pseudo-remainder by a^d, where d is the number of cancellation rounds.

The Mathlib companion transports the same step through the formal-degree Sylvester determinant. This is the resultant recurrence used by the later Brown correctness argument; the coefficientwise integrality of Brown's exact quotients remains its own subresultant theorem.

theorem

Hex.DensePoly.PseudoDivMod.quotient_degree.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (f g : Hex.DensePoly R) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  (HexPolyMathlib.toPolynomial (f.pseudoDivMod g).1).natDegree +
      (HexPolyMathlib.toPolynomial g).natDegree ≤
    (HexPolyMathlib.toPolynomial f).natDegree
Hex.DensePoly.PseudoDivMod.quotient_degree.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (f g : Hex.DensePoly R)
  (hg : g ≠ 0) (hgf : g.size ≤ f.size) :
  (HexPolyMathlib.toPolynomial
          (f.pseudoDivMod
              g).1).natDegree +
      (HexPolyMathlib.toPolynomial
          g).natDegree ≤
    (HexPolyMathlib.toPolynomial
        f).natDegree

A pseudo-quotient fits in the formal-degree gap required by Mathlib's resultant row-operation theorem.

theorem

Hex.DensePoly.PseudoDivMod.remainder_degree.{u} {R : Type u}
  [CommRing R] [DecidableEq R] (f g : Hex.DensePoly R) (hg : g ≠ 0) :
  HexPolyMathlib.toPolynomial (f.pseudoDivMod g).2 = 0 ∨
    (HexPolyMathlib.toPolynomial (f.pseudoDivMod g).2).natDegree <
      (HexPolyMathlib.toPolynomial g).natDegree
Hex.DensePoly.PseudoDivMod.remainder_degree.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (f g : Hex.DensePoly R)
  (hg : g ≠ 0) :
  HexPolyMathlib.toPolynomial
        (f.pseudoDivMod g).2 =
      0 ∨
    (HexPolyMathlib.toPolynomial
          (f.pseudoDivMod
              g).2).natDegree <
      (HexPolyMathlib.toPolynomial
          g).natDegree

A pseudo-remainder is zero or has strictly smaller Mathlib degree than the nonzero divisor. The disjunction records Mathlib's default degree 0 for the zero polynomial, including the constant-divisor case.

theorem

Hex.DensePoly.PseudoDivMod.resultant_step.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (f g : Hex.DensePoly R) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  have r := (f.pseudoDivMod g).2;
  have F := HexPolyMathlib.toPolynomial f;
  have G := HexPolyMathlib.toPolynomial g;
  have P := HexPolyMathlib.toPolynomial r;
  have n := F.natDegree;
  have m := G.natDegree;
  (g.leadingCoeff ^ (f.size - g.size + 1)) ^ m * F.resultant G n m =
    (-1) ^ (n * m) * G.resultant P m n
Hex.DensePoly.PseudoDivMod.resultant_step.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (f g : Hex.DensePoly R)
  (hg : g ≠ 0) (hgf : g.size ≤ f.size) :
  have r := (f.pseudoDivMod g).2;
  have F := HexPolyMathlib.toPolynomial f;
  have G := HexPolyMathlib.toPolynomial g;
  have P := HexPolyMathlib.toPolynomial r;
  have n := F.natDegree;
  have m := G.natDegree;
  (g.leadingCoeff ^
          (f.size - g.size + 1)) ^
        m *
      F.resultant G n m =
    (-1) ^ (n * m) * G.resultant P m n

One fraction-free pseudo-division step transports the formal-degree resultant from (f,g) to (g,r), including the Sylvester swap sign.

theorem

Hex.DensePoly.PseudoDivMod.resultant_step_degree.{u} {R : Type u}
  [CommRing R] [DecidableEq R] (f g : Hex.DensePoly R) (hg : g ≠ 0)
  (hgf : g.size ≤ f.size) :
  have r := (f.pseudoDivMod g).2;
  have F := HexPolyMathlib.toPolynomial f;
  have G := HexPolyMathlib.toPolynomial g;
  have P := HexPolyMathlib.toPolynomial r;
  have n := F.natDegree;
  have m := G.natDegree;
  have k := P.natDegree;
  (g.leadingCoeff ^ (f.size - g.size + 1)) ^ m * F.resultant G n m =
    (-1) ^ (n * m) * (g.leadingCoeff ^ (n - k) * G.resultant P m k)
Hex.DensePoly.PseudoDivMod.resultant_step_degree.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (f g : Hex.DensePoly R)
  (hg : g ≠ 0) (hgf : g.size ≤ f.size) :
  have r := (f.pseudoDivMod g).2;
  have F := HexPolyMathlib.toPolynomial f;
  have G := HexPolyMathlib.toPolynomial g;
  have P := HexPolyMathlib.toPolynomial r;
  have n := F.natDegree;
  have m := G.natDegree;
  have k := P.natDegree;
  (g.leadingCoeff ^
          (f.size - g.size + 1)) ^
        m *
      F.resultant G n m =
    (-1) ^ (n * m) *
      (g.leadingCoeff ^ (n - k) *
        G.resultant P m k)

The pseudo-division resultant identity with the remainder returned to its actual default degree. The compensating leading-coefficient power records the formal-degree promotion explicitly.

21.1.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.

21.1.5. Certified chain structure🔗

The chain representation comes with structural guarantees, not only executable checks. Every stored term is nonzero; after the two ordered inputs, each stored polynomial is strictly smaller than its predecessor; and a nonzero input pair produces at most min(deg f, deg g) + 2 terms.

theorem

Hex.DensePoly.subresultantChain_ne_zero.{u} {S : Type u} [Zero S]
  [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g p : Hex.DensePoly S) (hp : p ∈ f.subresultantChain g) : p ≠ 0
Hex.DensePoly.subresultantChain_ne_zero.{u}
  {S : Type u} [Zero S] [DecidableEq S]
  [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g p : Hex.DensePoly S)
  (hp : p ∈ f.subresultantChain g) : p ≠ 0

Every stored term is nonzero. This follows from the worker's explicit zero guards and needs no divisibility laws.

theorem

Hex.DensePoly.subresultantChain_size_strict.{u} {S : Type u} [Zero S]
  [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g : Hex.DensePoly S) (i : ℕ) (hi : 1 ≤ i)
  (hnext : i + 1 < (f.subresultantChain g).size) :
  ((f.subresultantChain g).getD (i + 1) 0).size <
    ((f.subresultantChain g).getD i 0).size
Hex.DensePoly.subresultantChain_size_strict.{u}
  {S : Type u} [Zero S] [DecidableEq S]
  [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g : Hex.DensePoly S) (i : ℕ)
  (hi : 1 ≤ i)
  (hnext :
    i + 1 <
      (f.subresultantChain g).size) :
  ((f.subresultantChain g).getD (i + 1)
        0).size <
    ((f.subresultantChain g).getD i
        0).size

After the possibly equal-degree ordered inputs, stored degrees strictly decrease.

theorem

Hex.DensePoly.subresultantChain_size_le.{u} {S : Type u} [Zero S]
  [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g : Hex.DensePoly S) (hf : f ≠ 0) (hg : g ≠ 0) :
  (f.subresultantChain g).size ≤
    min (f.degree?.getD 0) (g.degree?.getD 0) + 2
Hex.DensePoly.subresultantChain_size_le.{u}
  {S : Type u} [Zero S] [DecidableEq S]
  [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g : Hex.DensePoly S) (hf : f ≠ 0)
  (hg : g ≠ 0) :
  (f.subresultantChain g).size ≤
    min (f.degree?.getD 0)
        (g.degree?.getD 0) +
      2

The nonzero Brown chain stores at most two inputs plus one term for every possible degree at or below the smaller input degree.

21.1.5.1. Fuel control🔗

The implementation bounds its recursion with an explicit fuel parameter. subresultantOrdered selects the public g.size + 1 budget; subresultantOrderedFuel exposes the same recurrence with an explicit budget for proof auditing. Adding fuel beyond the public budget leaves the result unchanged.

def

Hex.DensePoly.subresultantOrdered.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) : Hex.PRSResult R
Hex.DensePoly.subresultantOrdered.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) :
  Hex.PRSResult R

Brown's recurrence for two nonzero inputs already ordered by decreasing dense degree. One fuel unit per possible degree, plus the terminal step, is sufficient on a lawful exact-division domain.

def

Hex.DensePoly.subresultantOrderedFuel.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) (fuel : ℕ) : Hex.PRSResult R
Hex.DensePoly.subresultantOrderedFuel.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) (fuel : ℕ) :
  Hex.PRSResult R

Brown's recurrence for two nonzero inputs already ordered by decreasing dense degree, with an explicit proof-audit fuel parameter.

theorem

Hex.DensePoly.subresultantOrderedFuel_eq.{u} {S : Type u} [Zero S]
  [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g : Hex.DensePoly S) (hg : g ≠ 0) (extra : ℕ) :
  f.subresultantOrderedFuel g (g.size + 1 + extra) =
    f.subresultantOrdered g
Hex.DensePoly.subresultantOrderedFuel_eq.{u}
  {S : Type u} [Zero S] [DecidableEq S]
  [One S] [Add S] [Sub S] [Mul S] [Div S]
  (f g : Hex.DensePoly S) (hg : g ≠ 0)
  (extra : ℕ) :
  f.subresultantOrderedFuel g
      (g.size + 1 + extra) =
    f.subresultantOrdered g

Adding fuel beyond the public ordered-run budget leaves the result unchanged. This is a structural consequence of strict remainder-size descent and needs no divisibility laws.

Most callers need only the scalar resultant:

def

Hex.DensePoly.resultant.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R] (f g : Hex.DensePoly R) : R
Hex.DensePoly.resultant.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) : R

Executable polynomial resultant with default formal-degree conventions.

Zero polynomials are treated as degree zero, so two constants (including two zeros) have resultant one. Reversed nonzero inputs are ordered for the Brown run and receive the standard degree-product sign.

The discriminant uses the standard signed derivative-resultant formula, with the zero and constant conventions handled explicitly:

def

Hex.DensePoly.disc.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] [NatCast R] (f : Hex.DensePoly R) : R
Hex.DensePoly.disc.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R] [NatCast R]
  (f : Hex.DensePoly R) : R

Standard polynomial discriminant, with value one for zero and constants.

The leading-coefficient gap power promotes the derivative's default-degree resultant to formal derivative degree n - 1. This matters in positive characteristic, where the derivative's actual degree can drop.

21.1.6. A small exact computation🔗

For f = X² - 2 and g = X - 3, the resultant is f(3) = 7; the discriminant of f is 8. Both checks below run the Mathlib-free algorithm.

open Hex

namespace HexResultantChapter

private def f : DensePoly Int := DensePoly.ofList [-2, 0, 1]
private def g : DensePoly Int := DensePoly.ofList [-3, 1]

#guard DensePoly.resultant f g = 7
#guard DensePoly.disc f = 8

end HexResultantChapter

21.1.7. Companion contracts🔗

These declarations describe the executable results in Mathlib terms. The central contract identifies the executable scalar with Mathlib's determinant-defined resultant:

theorem

Hex.DensePoly.toPolynomial_resultant.{u} {R : Type u} [CommRing R]
  [IsDomain R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly R) :
  f.resultant g =
    (HexPolyMathlib.toPolynomial f).resultant
      (HexPolyMathlib.toPolynomial g) (f.degree?.getD 0)
      (g.degree?.getD 0)
Hex.DensePoly.toPolynomial_resultant.{u}
  {R : Type u} [CommRing R] [IsDomain R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly R) :
  f.resultant g =
    (HexPolyMathlib.toPolynomial
          f).resultant
      (HexPolyMathlib.toPolynomial g)
      (f.degree?.getD 0)
      (g.degree?.getD 0)

The executable and Mathlib resultants agree under dense-polynomial correspondence, with the executable default formal degrees made explicit.

The executable discriminant has the same total zero/constant convention as Mathlib's determinant-defined discriminant:

theorem

Hex.DensePoly.toPolynomial_disc.{u} {R : Type u} [CommRing R]
  [IsDomain R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  (f : Hex.DensePoly R) : f.disc = (HexPolyMathlib.toPolynomial f).discr
Hex.DensePoly.toPolynomial_disc.{u}
  {R : Type u} [CommRing R] [IsDomain R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  (f : Hex.DensePoly R) :
  f.disc =
    (HexPolyMathlib.toPolynomial f).discr

The executable and Mathlib discriminants agree under dense-polynomial correspondence.

For positive-degree polynomials in characteristic zero, discriminants multiply with the square of the cross-resultant. The degree hypotheses exclude the nonunit-constant counterexample created by the total constant convention. Over a characteristic-zero field, nonvanishing is therefore the expected separability criterion:

theorem

Hex.DensePoly.disc_mul.{u} {R : Type u} [CommRing R] [IsDomain R]
  [IsAddTorsionFree R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly R) (hf : 0 < f.degree?.getD 0)
  (hg : 0 < g.degree?.getD 0) :
  (f * g).disc = f.disc * g.disc * f.resultant g ^ 2
Hex.DensePoly.disc_mul.{u} {R : Type u}
  [CommRing R] [IsDomain R]
  [IsAddTorsionFree R] [DecidableEq R]
  [Div R] [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly R)
  (hf : 0 < f.degree?.getD 0)
  (hg : 0 < g.degree?.getD 0) :
  (f * g).disc =
    f.disc * g.disc * f.resultant g ^ 2

Discriminants multiply with the square of the cross-resultant.

The positive-degree hypotheses are essential: Mathlib and the executable API assign discriminant one to constants, while multiplying by a nonunit constant scales the other discriminant.

theorem

Hex.DensePoly.disc_ne_zero_iff_separable.{u} {R : Type u} [Field R]
  [IsAddTorsionFree R] [DecidableEq R] [Hex.ExactDivLaws R]
  (f : Hex.DensePoly R) (hf : 0 < f.degree?.getD 0) :
  f.disc ≠ 0 ↔ (HexPolyMathlib.toPolynomial f).Separable
Hex.DensePoly.disc_ne_zero_iff_separable.{u}
  {R : Type u} [Field R]
  [IsAddTorsionFree R] [DecidableEq R]
  [Hex.ExactDivLaws R]
  (f : Hex.DensePoly R)
  (hf : 0 < f.degree?.getD 0) :
  f.disc ≠ 0 ↔
    (HexPolyMathlib.toPolynomial
        f).Separable

A positive-degree polynomial over a characteristic-zero field has nonzero executable discriminant exactly when it is separable.

The specialization contract retains the original formal degrees, so degree drops after substituting a parameter do not silently change the resultant convention:

theorem

Hex.DensePoly.eval_resultant.{u} {R : Type u} [CommRing R] [IsDomain R]
  [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly (Hex.DensePoly R)) (a : R) :
  (f.resultant g).eval a =
    (f.specialize a).resultant (g.specialize a) (f.degree?.getD 0)
      (g.degree?.getD 0)
Hex.DensePoly.eval_resultant.{u}
  {R : Type u} [CommRing R] [IsDomain R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly (Hex.DensePoly R))
  (a : R) :
  (f.resultant g).eval a =
    (f.specialize a).resultant
      (g.specialize a) (f.degree?.getD 0)
      (g.degree?.getD 0)

Specializing the coefficient variable after elimination agrees with the formal-degree Mathlib resultant of the specialized inputs.

Mathlib's resultant has the following proved root-product formula. Together with the executable correspondence, this identity underlies one-level field norms and the Trager collision bound:

theorem

Hex.DensePoly.resultant_eq_leadingCoeff_mul_prod_roots.{u} {K : Type u}
  [Field K] [IsAlgClosed K] (f g : Polynomial K) :
  f.resultant g =
    f.leadingCoeff ^ g.natDegree *
      (Multiset.map (fun x => Polynomial.eval x g) f.roots).prod
Hex.DensePoly.resultant_eq_leadingCoeff_mul_prod_roots.{u}
  {K : Type u} [Field K] [IsAlgClosed K]
  (f g : Polynomial K) :
  f.resultant g =
    f.leadingCoeff ^ g.natDegree *
      (Multiset.map
          (fun x => Polynomial.eval x g)
          f.roots).prod

The resultant as the leading-coefficient power times evaluation over all roots of the first polynomial, counted with multiplicity.

21.1.8. Cross-references🔗

HexPoly supplies the normalized dense representation; HexResultant supplies the exact pseudo-division and Brown recurrence.
HexNumberField uses bivariate specialization vanishing to justify factorization-lazy arithmetic.
HexNumberFieldTower uses the full value and root-product correspondence for relative norms and Trager recovery.