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

Polynomial pseudo-division without coefficient division.

For g != 0 and g.degree? <= f.degree?, let d = f.degree - g.degree + 1. Over a commutative ring its result (q, r) satisfies

lc(g) ^ (f.degree - g.degree + 1) * f = q * g + r

with r.degree? < g.degree?. The implementation asks only for the concrete operations it executes; algebraic laws belong to the correctness theorems. Its nested array folds have O(d*m) summands, matching the pseudo-division complexity contract.

For the two inputs outside that contract, behavior is deliberately simple and stable: pseudoDivMod f 0 = (0, f), and if f is already smaller than a nonzero g, then pseudoDivMod f g = (0, f).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.DensePoly.pseudoDivMod_zero_right {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (f : DensePoly R) : f.pseudoDivMod 0 = (0, f)

A zero divisor takes the documented junk branch and leaves the dividend unchanged.

theorem Hex.DensePoly.pseudoDivMod_of_size_lt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (f g : DensePoly R) (h : f.size < g.size) : f.pseudoDivMod g = (0, f)

If the dividend is already smaller, pseudo-division is ordinary division by inspection.

theorem Hex.DensePoly.pseudoDivMod_reconstruct {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (f g : DensePoly S) (hg : g ≠ 0) (hfg : g.size ≤ f.size) : scale (g.leadingCoeff ^ (f.size - g.size + 1)) f = (f.pseudoDivMod g).fst * g + (f.pseudoDivMod g).snd

Pseudo-division reconstructs the fixed leading-coefficient multiple of the dividend.

This theorem deliberately uses a fresh coefficient type: an ambient Zero instance is not necessarily coherent with the zero supplied by Lean.Grind.CommRing.

theorem Hex.DensePoly.pseudoDivMod_quotient_size_le {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (f g : DensePoly R) : (f.pseudoDivMod g).fst.size ≤ f.size - g.size + 1

The quotient array is structurally bounded by the number of pseudo-division rounds. This bound does not use reconstruction correctness.

theorem Hex.DensePoly.pseudoDivMod_remainder_lt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (f g : DensePoly R) (hg : g ≠ 0) : (f.pseudoDivMod g).snd.size < g.size

The remainder array is structurally shorter than every nonzero divisor. This follows from the output fold's iteration count and does not constrain the computed coefficient values; reconstruction supplies the algebraic content.