hex

6.3. Arithmetic🔗

Addition is a linear merge of the two term lists; degree never appears in the cost. Multiplication's kernel-facing specification forms all pairwise products and canonicalises; the compiled implementation, selected by measurement in the project's benchmarking phase, folds the pairwise products into an Std.ExtTreeMap accumulator, which beat both the sort-and-combine route and a Johnson-style heap merge by about three times on low- and high-collision inputs alike.

🔗def
Hex.SparsePoly.add.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  (s t : Hex.SparsePoly R) : Hex.SparsePoly R
Hex.SparsePoly.add.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R]
  (s t : Hex.SparsePoly R) :
  Hex.SparsePoly R

Add two sparse polynomials by a linear merge of the sorted term arrays, O(s + t): sums at a matching exponent, and a zero sum stores nothing.

🔗def
Hex.SparsePoly.mul.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  [Mul R] (s t : Hex.SparsePoly R) : Hex.SparsePoly R
Hex.SparsePoly.mul.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R] [Mul R]
  (s t : Hex.SparsePoly R) :
  Hex.SparsePoly R

Multiply two sparse polynomials: the canonicalised pairwise product. Every pair of exponents contributes, exponent sums collide freely, and ofTerms combines the collisions and drops what cancels. The pairwise products are built through the term Lists so the kernel can reduce this specification (Array.flatMap stalls kernel reduction; the value is unchanged). The @[csimp] implementation is selected by the Phase-4 sparse-multiplication bench family; until then compiled code runs this specification through ofTerms's sort-and-combine twin.

🔗def
Hex.SparsePoly.mulMonomial.{u} {R : Type u} [Zero R] [DecidableEq R]
  [Mul R] (e : ℕ) (c : R) (s : Hex.SparsePoly R) : Hex.SparsePoly R
Hex.SparsePoly.mulMonomial.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [Mul R] (e : ℕ) (c : R)
  (s : Hex.SparsePoly R) :
  Hex.SparsePoly R

Multiply by the monomial c · x^e: add e to every exponent and multiply every coefficient by c. The exponent shift is strictly monotone, so the only canonicalisation is the zero filter. This is the cheap shift mul is built from, O(s).

🔗def
Hex.SparsePoly.scale.{u} {R : Type u} [Zero R] [DecidableEq R] [Mul R]
  (c : R) (s : Hex.SparsePoly R) : Hex.SparsePoly R
Hex.SparsePoly.scale.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Mul R] (c : R)
  (s : Hex.SparsePoly R) :
  Hex.SparsePoly R

Multiply every coefficient by c, dropping the products that vanish: c = 0 gives the zero polynomial, and a zero divisor c can delete an interior term while leaving its neighbours.

🔗def
Hex.SparsePoly.pow.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Mul R] (s : Hex.SparsePoly R) (n : ℕ) : Hex.SparsePoly R
Hex.SparsePoly.pow.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Mul R] (s : Hex.SparsePoly R) (n : ℕ) :
  Hex.SparsePoly R

Raise to a power by binary powering over mul. A caller wanting f(x^k) should use substPow, never pow: the cost difference is the whole reason this library exists.

The coefficient laws and the commutative-ring laws are proved under the Lean.Grind algebra classes; coeff_mul and the multiplicative laws are transported through the dense conversion.

🔗theorem
Hex.SparsePoly.coeff_mul.{u} {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S] (s t : Hex.SparsePoly S) (n : ℕ) :
  (s * t).coeff n = s.toDense.mulCoeffSum t.toDense n
Hex.SparsePoly.coeff_mul.{u} {S : Type u}
  [Lean.Grind.CommRing S] [DecidableEq S]
  (s t : Hex.SparsePoly S) (n : ℕ) :
  (s * t).coeff n =
    s.toDense.mulCoeffSum t.toDense n

The convolution, by transport: multiplication agrees with the dense coefficient sum.