@[irreducible]

def Hex.SparsePoly.mergeWith {R : Type u} [Zero R] [DecidableEq R] (fl fr : R → R) (fb : R → R → R) : List (Nat × R) → List (Nat × R) → List (Nat × R)

Linear merge of two sorted term lists: fl maps a coefficient present only on the left, fr one present only on the right, fb combines a collision, and zero results are dropped. add and sub are instances.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SparsePoly.mergeWith fl fr fb [] x✝ = List.filterMap (fun (t : Nat × R) => if fr t.snd = 0 then none else some (t.fst, fr t.snd)) x✝
• Hex.SparsePoly.mergeWith fl fr fb (a :: as) [] = List.filterMap (fun (t : Nat × R) => if fl t.snd = 0 then none else some (t.fst, fl t.snd)) (a :: as)

theorem Hex.SparsePoly.exp_mem_mergeWith {R : Type u} [Zero R] [DecidableEq R] {fl fr : R → R} {fb : R → R → R} {l₁ l₂ : List (Nat × R)} {t : Nat × R} (ht : t ∈ mergeWith fl fr fb l₁ l₂) : (∃ (u : Nat × R), u ∈ l₁ ∧ t.fst = u.fst) ∨ ∃ (u : Nat × R), u ∈ l₂ ∧ t.fst = u.fst

Every exponent stored by the merge comes from one of the inputs.

theorem Hex.SparsePoly.mergeWith_canonical {R : Type u} [Zero R] [DecidableEq R] {fl fr : R → R} {fb : R → R → R} {l₁ l₂ : List (Nat × R)} (hs₁ : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l₁) (hs₂ : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l₂) : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) (mergeWith fl fr fb l₁ l₂) ∧ ∀ (t : Nat × R), t ∈ mergeWith fl fr fb l₁ l₂ → t.snd ≠ 0

The merge of two canonical term lists is canonical.

theorem Hex.SparsePoly.coeffList_filterMap_map {R : Type u} [Zero R] [DecidableEq R] {f : R → R} {l : List (Nat × R)} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l) (hf0 : f 0 = 0) (e : Nat) : coeffList (List.filterMap (fun (t : Nat × R) => if f t.snd = 0 then none else some (t.fst, f t.snd)) l) e = f (coeffList l e)

Coefficient description of the zero-filtered coefficient map used by the merge's one-sided cases.

theorem Hex.SparsePoly.coeffList_mergeWith {R : Type u} [Zero R] [DecidableEq R] {fl fr : R → R} {fb : R → R → R} {l₁ l₂ : List (Nat × R)} (hs₁ : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l₁) (hs₂ : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l₂) (hb00 : fb 0 0 = 0) (hbl : ∀ (x : R), fb x 0 = fl x) (hbr : ∀ (y : R), fb 0 y = fr y) (e : Nat) : coeffList (mergeWith fl fr fb l₁ l₂) e = fb (coeffList l₁ e) (coeffList l₂ e)

Coefficient description of the merge. The three compatibility hypotheses identify the structural choices with the pointwise fb against an absent side's 0.

theorem Hex.SparsePoly.pairwise_toList {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) s.terms.toList

The canonical-form invariant, list-level: exponents strictly increase.

theorem Hex.SparsePoly.nonzero_toList {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) (t : Nat × R) : t ∈ s.terms.toList → t.snd ≠ 0

The canonical-form invariant, list-level: no stored coefficient is zero.

theorem Hex.SparsePoly.mem_support_iff {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) (e : Nat) : e ∈ s.support.toList ↔ s.coeff e ≠ 0

The stored exponents are exactly the exponents with a nonzero coefficient. Uses both canonical-form invariants: strict increase makes the stored coefficient the coefficient, and zero-freedom makes it nonzero.

def Hex.SparsePoly.ofCanonicalList {R : Type u} [Zero R] [DecidableEq R] (l : List (Nat × R)) (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l) (hnz : ∀ (t : Nat × R), t ∈ l → t.snd ≠ 0) : SparsePoly R

Package a canonical term list as a polynomial.

Equations

• Hex.SparsePoly.ofCanonicalList l hs hnz = { terms := l.toArray, canonical := ⋯ }

@[simp]

theorem Hex.SparsePoly.coeff_ofCanonicalList {R : Type u} [Zero R] [DecidableEq R] (l : List (Nat × R)) (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l) (hnz : ∀ (t : Nat × R), t ∈ l → t.snd ≠ 0) (e : Nat) : (ofCanonicalList l hs hnz).coeff e = coeffList l e

Packaging a canonical term list keeps its list coefficients.

def Hex.SparsePoly.mapTerms {R : Type u} [Zero R] [DecidableEq R] (g : Nat → Nat) (f : Nat → R → R) (l : List (Nat × R)) : List (Nat × R)

Map exponents and coefficients over a term list, dropping the terms whose new coefficient is zero. neg, scale, and mulMonomial are instances (with the identity exponent map or a shift).

Equations

• Hex.SparsePoly.mapTerms g f l = List.filterMap (fun (t : Nat × R) => if f t.fst t.snd = 0 then none else some (g t.fst, f t.fst t.snd)) l

theorem Hex.SparsePoly.exp_mem_mapTerms {R : Type u} [Zero R] [DecidableEq R] {g : Nat → Nat} {f : Nat → R → R} {l : List (Nat × R)} {t : Nat × R} (ht : t ∈ mapTerms g f l) : ∃ (u : Nat × R), u ∈ l ∧ t.fst = g u.fst

Every exponent stored by the map is the image of a stored one.

theorem Hex.SparsePoly.mapTerms_canonical {R : Type u} [Zero R] [DecidableEq R] {g : Nat → Nat} {f : Nat → R → R} {l : List (Nat × R)} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l) (hmono : ∀ (a : Nat × R), a ∈ l → ∀ (b : Nat × R), b ∈ l → a.fst < b.fst → g a.fst < g b.fst) : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) (mapTerms g f l) ∧ ∀ (t : Nat × R), t ∈ mapTerms g f l → t.snd ≠ 0

The map of a canonical term list along a strictly monotone exponent map is canonical.

theorem Hex.SparsePoly.coeffList_mapTerms_apply {R : Type u} [Zero R] [DecidableEq R] {g : Nat → Nat} {f : Nat → R → R} {l : List (Nat × R)} {e : Nat} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l) (hinj : ∀ (u : Nat × R), u ∈ l → g u.fst = g e → u.fst = e) (hf0 : f e 0 = 0) : coeffList (mapTerms g f l) (g e) = f e (coeffList l e)

Coefficient of the mapped list at a mapped exponent, for an exponent map injective into the stored exponents.

theorem Hex.SparsePoly.coeffList_mapTerms_of_ne {R : Type u} [Zero R] [DecidableEq R] {g : Nat → Nat} {f : Nat → R → R} {l : List (Nat × R)} {x : Nat} (hx : ∀ (u : Nat × R), u ∈ l → g u.fst ≠ x) : coeffList (mapTerms g f l) x = 0

The mapped list stores nothing outside the image of the exponent map.

def Hex.SparsePoly.add {R : Type u} [Zero R] [DecidableEq R] [Add R] (s t : SparsePoly R) : 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.

Equations

• s.add t = Hex.SparsePoly.ofCanonicalList (Hex.SparsePoly.mergeWith id id (fun (x1 x2 : R) => x1 + x2) s.terms.toList t.terms.toList) ⋯ ⋯

@[instance_reducible]

instance Hex.SparsePoly.instAdd {R : Type u} [Zero R] [DecidableEq R] [Add R] : Add (SparsePoly R)

Equations

• Hex.SparsePoly.instAdd = { add := Hex.SparsePoly.add }

theorem Hex.SparsePoly.coeff_add' {R : Type u} [Zero R] [DecidableEq R] [Add R] (h00 : 0 + 0 = 0) (hl : ∀ (x : R), x + 0 = x) (hr : ∀ (y : R), 0 + y = y) (s t : SparsePoly R) (e : Nat) : (s + t).coeff e = s.coeff e + t.coeff e

Coefficient law for add, under the pointwise hypotheses it needs; the Lean.Grind.Semiring form is coeff_add.

@[simp]

theorem Hex.SparsePoly.coeff_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s t : SparsePoly S) (e : Nat) : (s + t).coeff e = s.coeff e + t.coeff e

Grind-classes form of coeff_add': addition is coefficientwise.

def Hex.SparsePoly.sub {R : Type u} [Zero R] [DecidableEq R] [Sub R] (s t : SparsePoly R) : SparsePoly R

Subtract two sparse polynomials by a linear merge, O(s + t).

Equations

• s.sub t = Hex.SparsePoly.ofCanonicalList (Hex.SparsePoly.mergeWith id (fun (y : R) => 0 - y) (fun (x1 x2 : R) => x1 - x2) s.terms.toList t.terms.toList) ⋯ ⋯

@[instance_reducible]

instance Hex.SparsePoly.instSub {R : Type u} [Zero R] [DecidableEq R] [Sub R] : Sub (SparsePoly R)

Equations

• Hex.SparsePoly.instSub = { sub := Hex.SparsePoly.sub }

theorem Hex.SparsePoly.coeff_sub' {R : Type u} [Zero R] [DecidableEq R] [Sub R] (h00 : 0 - 0 = 0) (hl : ∀ (x : R), x - 0 = x) (s t : SparsePoly R) (e : Nat) : (s - t).coeff e = s.coeff e - t.coeff e

Coefficient law for sub, under the pointwise hypotheses it needs; the Lean.Grind.Ring form is coeff_sub.

@[simp]

theorem Hex.SparsePoly.coeff_sub {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (s t : SparsePoly S) (e : Nat) : (s - t).coeff e = s.coeff e - t.coeff e

Grind-classes form of coeff_sub': subtraction is coefficientwise.

def Hex.SparsePoly.neg {R : Type u} [Zero R] [DecidableEq R] [Sub R] (s : SparsePoly R) : SparsePoly R

Negate a sparse polynomial: subtraction from zero, compiled as one filtered coefficient map. Over a ring the exponents and the term count are unchanged; [Sub R] alone does not supply that, so the zero filter stays.

Equations

• s.neg = Hex.SparsePoly.ofCanonicalList (Hex.SparsePoly.mapTerms id (fun (x : Nat) (c : R) => 0 - c) s.terms.toList) ⋯ ⋯

@[instance_reducible]

instance Hex.SparsePoly.instNegOfSub {R : Type u} [Zero R] [DecidableEq R] [Sub R] : Neg (SparsePoly R)

Equations

• Hex.SparsePoly.instNegOfSub = { neg := Hex.SparsePoly.neg }

theorem Hex.SparsePoly.coeff_neg' {R : Type u} [Zero R] [DecidableEq R] [Sub R] (h00 : 0 - 0 = 0) (s : SparsePoly R) (e : Nat) : (-s).coeff e = 0 - s.coeff e

Coefficient law for neg, under the pointwise hypothesis it needs; the Lean.Grind.Ring form is coeff_neg.

@[simp]

theorem Hex.SparsePoly.coeff_neg {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (s : SparsePoly S) (e : Nat) : (-s).coeff e = 0 - s.coeff e

Grind-classes form of coeff_neg': negation is coefficientwise.

def Hex.SparsePoly.scale {R : Type u} [Zero R] [DecidableEq R] [Mul R] (c : R) (s : SparsePoly R) : 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.

Equations

• Hex.SparsePoly.scale c s = Hex.SparsePoly.ofCanonicalList (Hex.SparsePoly.mapTerms id (fun (x : Nat) (x_1 : R) => c * x_1) s.terms.toList) ⋯ ⋯

theorem Hex.SparsePoly.coeff_scale' {R : Type u} [Zero R] [DecidableEq R] [Mul R] (hc0 : ∀ (c : R), c * 0 = 0) (c : R) (s : SparsePoly R) (e : Nat) : (scale c s).coeff e = c * s.coeff e

Coefficient law for scale, under the pointwise hypothesis it needs; the Lean.Grind.Semiring form is coeff_scale.

@[simp]

theorem Hex.SparsePoly.coeff_scale {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (c : S) (s : SparsePoly S) (e : Nat) : (scale c s).coeff e = c * s.coeff e

Grind-classes form of coeff_scale': scaling multiplies each coefficient.

def Hex.SparsePoly.mulMonomial {R : Type u} [Zero R] [DecidableEq R] [Mul R] (e : Nat) (c : R) (s : SparsePoly R) : 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).

Equations

• Hex.SparsePoly.mulMonomial e c s = Hex.SparsePoly.ofCanonicalList (Hex.SparsePoly.mapTerms (fun (e' : Nat) => e + e') (fun (x : Nat) (x_1 : R) => c * x_1) s.terms.toList) ⋯ ⋯

theorem Hex.SparsePoly.coeff_mulMonomial' {R : Type u} [Zero R] [DecidableEq R] [Mul R] (hc0 : ∀ (c : R), c * 0 = 0) (s : SparsePoly R) (e : Nat) (c : R) (f : Nat) : (mulMonomial e c s).coeff f = if e ≤ f then c * s.coeff (f - e) else 0

Coefficient law for mulMonomial, under the pointwise hypothesis it needs; the Lean.Grind.Semiring form is coeff_mulMonomial.

@[simp]

theorem Hex.SparsePoly.coeff_mulMonomial {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s : SparsePoly S) (e : Nat) (c : S) (f : Nat) : (mulMonomial e c s).coeff f = if e ≤ f then c * s.coeff (f - e) else 0

Grind-classes form of coeff_mulMonomial': a monomial multiple shifts and scales the coefficients.

def Hex.SparsePoly.mul {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (s t : SparsePoly R) : 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.

Equations

• s.mul t = Hex.SparsePoly.ofTerms (List.flatMap (fun (a : Nat × R) => List.map (fun (b : Nat × R) => (a.fst + b.fst, a.snd * b.snd)) t.terms.toList) s.terms.toList).toArray

@[instance_reducible]

instance Hex.SparsePoly.instMulOfAdd {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] : Mul (SparsePoly R)

Equations

• Hex.SparsePoly.instMulOfAdd = { mul := Hex.SparsePoly.mul }

def Hex.SparsePoly.mulTree {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (s t : SparsePoly R) : Std.ExtTreeMap Nat R compare

Tree accumulator for mulImpl: fold every pairwise product into an Std.ExtTreeMap keyed on the exponent sum, replaying addCoeff per key so the accumulated value is exactly the specification's input-order fold. A stored 0 encodes an exponent whose partial sum cancelled and is dropped at read-out.

Equations

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

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

Runtime implementation of mul, selected by the Phase-4 sparse-multiplication bench family (see the SPEC's measured note): the ExtTreeMap accumulation, which beat sort-and-combine on both collision shapes and the Johnson heap merge everywhere (value-equal to mul by mul_eq_impl, registered @[csimp]).

Equations

• s.mulImpl t = { terms := (List.filter (fun (u : Nat × R) => decide (u.snd ≠ 0)) (s.mulTree t).toList).toArray, canonical := ⋯ }

theorem Hex.SparsePoly.mul_eq_mulImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (s t : SparsePoly R) : s.mul t = s.mulImpl t

The specification and the tree accumulation compute the same polynomial, with no algebra assumed: the tree replays the addCoeff steps per key in the specification's input order.

@[csimp]

theorem Hex.SparsePoly.mul_eq_impl : @mul = @mulImpl

Register the tree accumulation as the compiled implementation of mul.

@[irreducible]

def Hex.SparsePoly.pow {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Mul R] (s : SparsePoly R) (n : Nat) : 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.

Equations

• s.pow n = if _h : n = 0 then 1 else if n % 2 = 1 then s.mul ((s.mul s).pow (n / 2)) else (s.mul s).pow (n / 2)

@[instance_reducible]

instance Hex.SparsePoly.instPowNatOfOneOfAddOfMul {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Mul R] : Pow (SparsePoly R) Nat

Equations

• Hex.SparsePoly.instPowNatOfOneOfAddOfMul = { pow := Hex.SparsePoly.pow }

@[instance_reducible]

instance Hex.SparsePoly.instDvdOfAddOfMul {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] : Dvd (SparsePoly R)

Divisibility by existence of a cofactor, matching the DensePoly convention.

Equations

• Hex.SparsePoly.instDvdOfAddOfMul = { dvd := fun (p q : Hex.SparsePoly R) => ∃ (r : Hex.SparsePoly R), q = p * r }

theorem Hex.SparsePoly.dvd_def {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : SparsePoly R) : p ∣ q ↔ ∃ (r : SparsePoly R), q = p * r

Divisibility unfolds to a cofactor witness.

theorem Hex.SparsePoly.add_comm {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s t : SparsePoly S) : s + t = t + s

Addition is commutative.

theorem Hex.SparsePoly.add_assoc {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s t u : SparsePoly S) : s + t + u = s + (t + u)

Addition is associative.

@[simp]

theorem Hex.SparsePoly.add_zero {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s : SparsePoly S) : s + 0 = s

Zero is a right identity for addition.

@[simp]

theorem Hex.SparsePoly.zero_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s : SparsePoly S) : 0 + s = s

Zero is a left identity for addition.