structure Hex.DensePoly.PseudoResult (R : Type u) [Zero R] [DecidableEq R] : Type u

The multiplier, quotient and remainder of a pseudo-division.

• multiplier : R
• quotient : DensePoly R
• remainder : DensePoly R

def Hex.DensePoly.pseudoExponent {R : Type u} [Zero R] [DecidableEq R] (p q : DensePoly R) : Nat

The fixed leading-coefficient exponent, including the zero/smaller-input cases.

Equations

• p.pseudoExponent q = if (q.isZero || decide (p.size < q.size)) = true then 0 else p.size - q.size + 1

def Hex.DensePoly.pseudoDiv {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) : PseudoResult R

Pseudo-division with its actual scalar multiplier. The quotient and remainder reuse pseudoDivMod. On a zero divisor or a smaller dividend the multiplier is one.

Equations

• p.pseudoDiv q = { multiplier := npowRec (p.pseudoExponent q) q.leadingCoeff, quotient := (p.pseudoDivMod q).fst, remainder := (p.pseudoDivMod q).snd }

@[simp]

theorem Hex.DensePoly.pseudoDiv_zero_right {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p : DensePoly R) : p.pseudoDiv 0 = { multiplier := 1, quotient := 0, remainder := p }

theorem Hex.DensePoly.pseudoDiv_of_size_lt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) (h : p.size < q.size) : p.pseudoDiv q = { multiplier := 1, quotient := 0, remainder := p }

An already smaller input requires no cancellation or scaling.

def Hex.DensePoly.positivePseudoDiv {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Neg R] (sign : R → Int) (p q : DensePoly R) : PseudoResult R

Choose a positive multiplier by negating all three outputs together when necessary. The leading-coefficient sign and exponent parity determine the correction, avoiding a sign query on the larger computed power.

Equations

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

theorem Hex.DensePoly.positivePseudoDiv_remainder_lt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Neg R] (sign : R → Int) (p q : DensePoly R) (hq : q ≠ 0) : (positivePseudoDiv sign p q).remainder.size < q.size

Sign correction cannot increase the stored remainder size, even before any interpretation or algebraic laws are supplied.

@[irreducible]

def Hex.DensePoly.pseudoGcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) : DensePoly R

Plain pseudo-gcd. Its recursion decreases the stored size of the second polynomial, with no user bound and no Bézout polynomials. Correctness over a domain is a fraction-field gcd statement, not a gcd statement in R[X].

Equations

• p.pseudoGcd q = if _h : q.isZero = true then p else q.pseudoGcd (p.pseudoDivMod q).snd

@[simp]

theorem Hex.DensePoly.pseudoGcd_zero_right {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p : DensePoly R) : p.pseudoGcd 0 = p

theorem Hex.DensePoly.pseudoGcd_step {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) (hq : q ≠ 0) : p.pseudoGcd q = q.pseudoGcd (p.pseudoDivMod q).snd

The recursive equation records an actual division step and its strict descent.

@[simp]

theorem Hex.DensePoly.pseudoGcd_zero_left {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (q : DensePoly R) : pseudoGcd 0 q = q

theorem Hex.DensePoly.pseudoDiv_multiplier_ne_zero {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (hone : 1 ≠ 0) (hmul : ∀ (a b : R), a ≠ 0 → b ≠ 0 → a * b ≠ 0) (p q : DensePoly R) (hq : q ≠ 0) : (p.pseudoDiv q).multiplier ≠ 0

A genuine coefficient domain has a nonzero pseudo-division multiplier; no division or field structure on the coefficient type is involved.

theorem Hex.DensePoly.pseudoDiv_remainder_lt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) (hq : q ≠ 0) : (p.pseudoDiv q).remainder.size < q.size

The remainder bound holds without algebraic assumptions on stored coefficients.

theorem Hex.DensePoly.pseudoDiv_multiplier {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) : (p.pseudoDiv q).multiplier = q.leadingCoeff ^ p.pseudoExponent q

The recorded operation-only power agrees with the ring's natural power.

theorem Hex.DensePoly.pseudoDiv_reconstruct {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (hq : q ≠ 0) : scale (p.pseudoDiv q).multiplier p = (p.pseudoDiv q).quotient * q + (p.pseudoDiv q).remainder

Reconstruction uses exactly the multiplier returned by pseudoDiv, including zero dividends and dividends smaller than the divisor.