24.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.natDegree g.natDegree + 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.natDegree g.natDegree + 2

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

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