hex

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