def Hex.SparsePolyCanonical {R : Type u} [Zero R] (terms : Array (Nat × R)) : Prop

A term array is canonical when its exponents are strictly increasing and no stored coefficient is zero.

Equations

• Hex.SparsePolyCanonical terms = (List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) terms.toList ∧ ∀ (t : Nat × R), t ∈ terms → t.snd ≠ 0)

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

A univariate polynomial over R as a canonical sorted array of (exponent, coefficient) terms, ascending in exponent. Exponents are Nat, so degrees like 10^6 cost nothing to store; only toDense materialises a coefficient vector.

Per design principle 10, consumers read terms through the API (coeff, support, numTerms, degree?, leadingCoeff, and the ordered toTerms and foldTerms), not directly, so the representation can change.

• terms : Array (Nat × R)

  The stored (exponent, coefficient) terms in strictly increasing exponent order, with no zero coefficients.

• canonical : SparsePolyCanonical self.terms

  Proof that terms is canonical.

@[instance_reducible]

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

Equations

• a.instDecidableEq b = match decEq a.terms b.terms with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

def Hex.SparsePoly.zero {R : Type u} [Zero R] [DecidableEq R] : SparsePoly R

The zero polynomial: the empty term array.

Equations

• Hex.SparsePoly.zero = { terms := #[], canonical := ⋯ }

@[instance_reducible]

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

Equations

• Hex.SparsePoly.instZero = { zero := Hex.SparsePoly.zero }

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

The number of stored terms, which is the size of the support.

Equations

• s.numTerms = s.terms.size

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

true exactly when the polynomial is zero.

Equations

• s.isZero = s.terms.isEmpty

def Hex.SparsePoly.support {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : Array Nat

The stored exponents in increasing order; exactly the exponents whose coefficient is nonzero.

Equations

• s.support = Array.map (fun (x : Nat × R) => x.fst) s.terms

def Hex.SparsePoly.degree? {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : Option Nat

The degree, or none for the zero polynomial. The terms ascend in exponent, so the degree is the last stored exponent.

Equations

• s.degree? = Option.map (fun (x : Nat × R) => x.fst) s.terms.back?

@[reducible, inline]

abbrev Hex.SparsePoly.natDegree {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : Nat

The degree, with the zero polynomial given degree 0, matching DensePoly.natDegree.

Equations

• s.natDegree = s.degree?.getD 0

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

The leading coefficient, which is 0 for the zero polynomial.

Equations

• s.leadingCoeff = match s.terms.back? with | some t => t.snd | none => 0

def Hex.SparsePoly.toTerms {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) : List (Nat × R)

The stored terms in increasing exponent order.

Equations

• s.toTerms = s.terms.toList

def Hex.SparsePoly.foldTerms {R : Type u} [Zero R] [DecidableEq R] {β : Type v} (s : SparsePoly R) (f : β → Nat → R → β) (init : β) : β

Fold over the stored terms in increasing exponent order, O(t).

Equations

• s.foldTerms f init = Array.foldl (fun (acc : β) (t : Nat × R) => f acc t.fst t.snd) init s.terms

def Hex.SparsePoly.coeffList {R : Type u} [Zero R] : List (Nat × R) → Nat → R

The coefficient at exponent e in a term list: the first stored match, 0 when absent. On a canonical list the match is unique.

Equations

• Hex.SparsePoly.coeffList [] x✝ = 0
• Hex.SparsePoly.coeffList (t :: ts) x✝ = if t.fst = x✝ then t.snd else Hex.SparsePoly.coeffList ts x✝

noncomputable def Hex.SparsePoly.coeff {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) (e : Nat) : R

The coefficient at e. Kernel-facing specification (an ordered List lookup); compiled code uses Hex.SparsePoly.coeffImpl, the value-equal binary search selected by Hex.SparsePoly.coeff_eq_impl.

Equations

• s.coeff e = Hex.SparsePoly.coeffList s.terms.toList e

@[irreducible]

def Hex.SparsePoly.coeffSearch {R : Type u} [Zero R] (ts : Array (Nat × R)) (e lo hi : Nat) : R

Binary-search worker for coeffImpl: find the coefficient at exponent e among indices in [lo, hi) of a term array sorted by strictly increasing exponent.

Equations

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

def Hex.SparsePoly.coeffImpl {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) (e : Nat) : R

Runtime implementation of coeff: binary search on the sorted term array, O(log t) (value-equal to coeff by coeff_eq_impl, registered @[csimp]).

Equations

• s.coeffImpl e = Hex.SparsePoly.coeffSearch s.terms e 0 s.terms.size

theorem Hex.SparsePoly.coeffList_eq_zero {R : Type u} [Zero R] {l : List (Nat × R)} {e : Nat} (h : ∀ (t : Nat × R), t ∈ l → t.fst ≠ e) : coeffList l e = 0

A term list with no term at exponent e has coefficient 0 there.

theorem Hex.SparsePoly.coeffList_eq_of_mem {R : Type u} [Zero R] {l : List (Nat × R)} {t : Nat × R} {e : Nat} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l) (ht : t ∈ l) (he : t.fst = e) : coeffList l e = t.snd

On a list with strictly increasing exponents, a stored term at exponent e is the coefficient there.

theorem Hex.SparsePoly.coeffSearch_eq_coeffList {R : Type u} [Zero R] (ts : Array (Nat × R)) (e : Nat) (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) ts.toList) (lo hi : Nat) (hhi : hi ≤ ts.size) (hrange : ∀ (i : Nat) (h : i < ts.size), ts[i].fst = e → lo ≤ i ∧ i < hi) : coeffSearch ts e lo hi = coeffList ts.toList e

On the range that the sortedness invariant confines the matching exponent to, the binary search agrees with the ordered List lookup.

theorem Hex.SparsePoly.coeff_eq_coeffImpl {R : Type u} [Zero R] [DecidableEq R] (s : SparsePoly R) (e : Nat) : s.coeff e = s.coeffImpl e

The kernel-facing List lookup and the binary search compute the same coefficient on every canonical polynomial.

@[csimp]

theorem Hex.SparsePoly.coeff_eq_impl : @coeff = @coeffImpl

Register the binary search as the compiled implementation of coeff.

def Hex.SparsePoly.isCanonicalList {R : Type u} [Zero R] [DecidableEq R] : List (Nat × R) → Bool

Linear canonicality check on a term list: adjacent exponents strictly increase and no stored coefficient is zero. The pairwise form of the invariant is the one induction wants; this adjacent form is the one an O(t) check wants, and isCanonicalList_iff is the equivalence.

Equations

• Hex.SparsePoly.isCanonicalList [] = true
• Hex.SparsePoly.isCanonicalList [t] = decide (t.snd ≠ 0)
• Hex.SparsePoly.isCanonicalList (a :: b :: ts) = (decide (a.snd ≠ 0) && decide (a.fst < b.fst) && Hex.SparsePoly.isCanonicalList (b :: ts))

theorem Hex.SparsePoly.isCanonicalList_iff {R : Type u} [Zero R] [DecidableEq R] {l : List (Nat × R)} : isCanonicalList l = true ↔ List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) l ∧ ∀ (t : Nat × R), t ∈ l → t.snd ≠ 0

The adjacent-pair check decides the pairwise invariant: < on Nat is transitive, so strict increase between neighbours is strict increase between every pair.

def Hex.SparsePoly.isCanonical {R : Type u} [Zero R] [DecidableEq R] (ts : Array (Nat × R)) : Bool

Linear canonicality check on a term array, O(t).

Equations

• Hex.SparsePoly.isCanonical ts = Hex.SparsePoly.isCanonicalList ts.toList

theorem Hex.SparsePoly.isCanonical_iff {R : Type u} [Zero R] [DecidableEq R] {ts : Array (Nat × R)} : isCanonical ts = true ↔ SparsePolyCanonical ts

The O(t) adjacent-pair check decides SparsePolyCanonical.

@[instance_reducible]

instance Hex.SparsePoly.instDecidableSparsePolyCanonical {R : Type u} [Zero R] [DecidableEq R] (ts : Array (Nat × R)) : Decidable (SparsePolyCanonical ts)

Equations

• Hex.SparsePoly.instDecidableSparsePolyCanonical ts = decidable_of_iff (Hex.SparsePoly.isCanonical ts = true) ⋯

theorem Hex.SparsePoly.coeffList_eq_zero_of_lt_head {R : Type u} [Zero R] {b : Nat × R} {bs : List (Nat × R)} {e : Nat} (hs : List.Pairwise (fun (x y : Nat × R) => x.fst < y.fst) (b :: bs)) (he : e < b.fst) : coeffList (b :: bs) e = 0

A sorted term list has coefficient 0 below its head exponent.

theorem Hex.SparsePoly.coeffList_tail_eq_zero {R : Type u} [Zero R] {a : Nat × R} {as : List (Nat × R)} (hs : List.Pairwise (fun (x y : Nat × R) => x.fst < y.fst) (a :: as)) : coeffList as a.fst = 0

The tail of a sorted term list has coefficient 0 at the head's exponent: strict increase means the head's exponent never recurs.

theorem Hex.SparsePoly.coeffList_ext {R : Type u} [Zero 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₂) (hnz₁ : ∀ (t : Nat × R), t ∈ l₁ → t.snd ≠ 0) (hnz₂ : ∀ (t : Nat × R), t ∈ l₂ → t.snd ≠ 0) (h : ∀ (e : Nat), coeffList l₁ e = coeffList l₂ e) : l₁ = l₂

Two canonical term lists with the same coefficient function are equal. This is the list-level content of SparsePoly.ext_coeff: strict exponent increase forbids duplicates and fixes the order, and the zero-free condition makes every stored term observable.

theorem Hex.SparsePoly.ext_coeff {R : Type u} [Zero R] [DecidableEq R] {s t : SparsePoly R} (h : ∀ (e : Nat), s.coeff e = t.coeff e) : s = t

Extensionality: canonical representations of the same coefficient function are equal. Everything below is proved from this.

theorem Hex.SparsePoly.ext_coeff_iff {R : Type u} [Zero R] [DecidableEq R] {s t : SparsePoly R} : s = t ↔ ∀ (e : Nat), s.coeff e = t.coeff e

def Hex.SparsePoly.addCoeff {R : Type u} [Zero R] [DecidableEq R] [Add R] (d c : R) : R

The coefficient stored at an exponent after adding c to a stored coefficient d there, where d = 0 encodes "absent": a zero sum (and a zero insertion) leaves the exponent absent, encoded as 0 again. On a canonical representation the stored coefficient is 0 exactly when the term is absent, so this is the whole observable effect of addTerm at its target exponent.

Equations

• Hex.SparsePoly.addCoeff d c = if d = 0 then if c = 0 then 0 else c else if d + c = 0 then 0 else d + c

def Hex.SparsePoly.addTermList {R : Type u} [Zero R] [DecidableEq R] [Add R] : List (Nat × R) → Nat → R → List (Nat × R)

Ordered insert of c · x^e into a sorted term list: insert a new term when c ≠ 0 and e is absent, replace the stored coefficient by the sum when the sum is nonzero, and delete the term when the sum is zero.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SparsePoly.addTermList [] x✝¹ x✝ = if x✝ = 0 then [] else [(x✝¹, x✝)]

theorem Hex.SparsePoly.exp_mem_addTermList {R : Type u} [Zero R] [DecidableEq R] [Add R] {l : List (Nat × R)} {e : Nat} {c : R} {t : Nat × R} (ht : t ∈ addTermList l e c) : t.fst = e ∨ ∃ (u : Nat × R), u ∈ l ∧ t.fst = u.fst

Every exponent stored after an insert was stored before or is the inserted one.

theorem Hex.SparsePoly.addTermList_canonical {R : Type u} [Zero R] [DecidableEq R] [Add 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) (c : R) : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) (addTermList l e c) ∧ ∀ (t : Nat × R), t ∈ addTermList l e c → t.snd ≠ 0

The ordered insert preserves both halves of the canonical invariant. This is the proof the whole library rests on: every specialised operation re-establishes what addTermList establishes here for arbitrary input.

noncomputable def Hex.SparsePoly.addTerm {R : Type u} [Zero R] [DecidableEq R] [Add R] (s : SparsePoly R) (e : Nat) (c : R) : SparsePoly R

Add c · x^e to s, combining with an existing term at e and deleting the term when the sum is zero.

Kernel-facing specification (a single ordered List insert); compiled code uses Hex.SparsePoly.addTermImpl, the value-equal binary search and in-place array update selected by Hex.SparsePoly.addTerm_eq_impl.

Equations

• s.addTerm e c = { terms := (Hex.SparsePoly.addTermList s.terms.toList e c).toArray, canonical := ⋯ }

theorem Hex.SparsePoly.eq_of_terms_eq {R : Type u} [Zero R] [DecidableEq R] {s t : SparsePoly R} (h : s.terms = t.terms) : s = t

Equal term arrays give equal polynomials: the proof field is irrelevant.

theorem Hex.SparsePoly.coeffList_addTermList {R : Type u} [Zero R] [DecidableEq R] [Add 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) (c : R) (f : Nat) : coeffList (addTermList l e c) f = if f = e then addCoeff (coeffList l e) c else coeffList l f

The whole observable effect of the ordered insert: the coefficient at e becomes addCoeff of the stored coefficient and c, and every other coefficient is unchanged.

theorem Hex.SparsePoly.coeff_addTerm {R : Type u} [Zero R] [DecidableEq R] [Add R] (s : SparsePoly R) (e : Nat) (c : R) (f : Nat) : (s.addTerm e c).coeff f = if f = e then addCoeff (s.coeff e) c else s.coeff f

Coefficient description of addTerm: addCoeff at the target exponent, unchanged elsewhere.

@[irreducible]

def Hex.SparsePoly.lowerBound {R : Type u} (ts : Array (Nat × R)) (e lo hi : Nat) : Nat

Binary-search worker for addTermImpl: the least index in [lo, hi) whose exponent is at least e (or hi when there is none), on an array sorted by strictly increasing exponent.

Equations

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

theorem Hex.SparsePoly.lowerBound_spec {R : Type u} (ts : Array (Nat × R)) (e : Nat) (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) ts.toList) (lo hi : Nat) (hlohi : lo ≤ hi) (hhi : hi ≤ ts.size) (hbelow : ∀ (i : Nat) (h : i < ts.size), i < lo → ts[i].fst < e) (habove : ∀ (i : Nat) (h : i < ts.size), hi ≤ i → e ≤ ts[i].fst) : lo ≤ lowerBound ts e lo hi ∧ lowerBound ts e lo hi ≤ hi ∧ (∀ (i : Nat) (h : i < ts.size), i < lowerBound ts e lo hi → ts[i].fst < e) ∧ ∀ (i : Nat) (h : i < ts.size), lowerBound ts e lo hi ≤ i → e ≤ ts[i].fst

On a sorted range, lowerBound splits the indices: every exponent below the returned position is below e, every exponent at or beyond it is at least e.

theorem Hex.SparsePoly.lowerBound_le {R : Type u} (ts : Array (Nat × R)) (e lo hi : Nat) (h : lo ≤ hi) : lowerBound ts e lo hi ≤ hi

lowerBound never exceeds hi, with no sortedness needed: this is what makes the insertion index valid.

theorem Hex.SparsePoly.addTermList_splice {R : Type u} [Zero R] [DecidableEq R] [Add R] {l : List (Nat × R)} {e p : Nat} (hbelow : ∀ (i : Nat) (h : i < l.length), i < p → l[i].fst < e) (habove : ∀ (i : Nat) (h : i < l.length), p ≤ i → e ≤ l[i].fst) (c : R) : addTermList l e c = match l[p]? with | some t => if t.fst = e then if t.snd + c = 0 then l.eraseIdx p else l.set p (e, t.snd + c) else if c = 0 then l else l.insertIdx p (e, c) | none => if c = 0 then l else l ++ [(e, c)]

The ordered insert, described at the splice position: with p splitting the sorted list into exponents below e and at least e, the insert is an index-p erase, set, insert, or append. This is the list-level shape that the in-place array implementation mirrors.

def Hex.SparsePoly.addTermArray {R : Type u} [Zero R] [DecidableEq R] [Add R] (ts : Array (Nat × R)) (e : Nat) (c : R) : Array (Nat × R)

In-place array worker for addTermImpl: binary search for the splice position, then a single erase, set, insert, or push. O(log t) search plus an O(t) shift.

Equations

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

theorem Hex.SparsePoly.addTermArray_eq {R : Type u} [Zero R] [DecidableEq R] [Add R] {ts : Array (Nat × R)} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) ts.toList) (e : Nat) (c : R) : addTermArray ts e c = (addTermList ts.toList e c).toArray

On a sorted array the in-place worker computes exactly the ordered List insert.

def Hex.SparsePoly.addTermImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] (s : SparsePoly R) (e : Nat) (c : R) : SparsePoly R

Runtime implementation of addTerm: binary search and one in-place array splice (value-equal to addTerm by addTerm_eq_impl, registered @[csimp]).

Equations

• s.addTermImpl e c = { terms := Hex.SparsePoly.addTermArray s.terms e c, canonical := ⋯ }

theorem Hex.SparsePoly.addTerm_eq_addTermImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] (s : SparsePoly R) (e : Nat) (c : R) : s.addTerm e c = s.addTermImpl e c

The ordered-List specification and the in-place splice compute the same polynomial.

@[csimp]

theorem Hex.SparsePoly.addTerm_eq_impl : @addTerm = @addTermImpl

Register the in-place splice as the compiled implementation of addTerm.

noncomputable def Hex.SparsePoly.ofTerms {R : Type u} [Zero R] [DecidableEq R] [Add R] (ts : Array (Nat × R)) : SparsePoly R

The canonical polynomial with the given terms. Exponents may repeat and may appear in any order, and coefficients at equal exponents are summed and zero results are dropped.

Kernel-facing specification (a fold of addTerm); compiled code uses Hex.SparsePoly.ofTermsImpl, the value-equal stable sort and combining pass selected by Hex.SparsePoly.ofTerms_eq_impl.

Equations

• Hex.SparsePoly.ofTerms ts = Array.foldl (fun (s : Hex.SparsePoly R) (t : Nat × R) => s.addTerm t.fst t.snd) 0 ts

@[simp]

theorem Hex.SparsePoly.coeff_zero {R : Type u} [Zero R] [DecidableEq R] (e : Nat) : coeff 0 e = 0

The zero polynomial has zero coefficients.

theorem Hex.SparsePoly.coeff_foldl_addTerm {R : Type u} [Zero R] [DecidableEq R] [Add R] (l : List (Nat × R)) (s : SparsePoly R) (e : Nat) : (List.foldl (fun (s : SparsePoly R) (t : Nat × R) => s.addTerm t.fst t.snd) s l).coeff e = List.foldl (fun (acc : R) (t : Nat × R) => addCoeff acc t.snd) (s.coeff e) (List.filter (fun (t : Nat × R) => decide (t.fst = e)) l)

Coefficient description of the addTerm fold, with no algebra assumed: at each exponent it is the addCoeff fold, in input order, over the terms at that exponent.

theorem Hex.SparsePoly.coeff_ofTerms_addCoeff {R : Type u} [Zero R] [DecidableEq R] [Add R] (ts : Array (Nat × R)) (e : Nat) : (ofTerms ts).coeff e = List.foldl (fun (acc : R) (t : Nat × R) => addCoeff acc t.snd) 0 (List.filter (fun (t : Nat × R) => decide (t.fst = e)) ts.toList)

Coefficient description of ofTerms, with no algebra assumed.

theorem Hex.SparsePoly.addCoeff_eq_add {R : Type u} [Zero R] [DecidableEq R] [Add R] (hzero : ∀ (c : R), 0 + c = c) (d c : R) : addCoeff d c = d + c

Once 0 is a left identity for +, the delete-and-reinsert step is plain addition.

theorem Hex.SparsePoly.coeff_ofTerms {R : Type u} [Zero R] [DecidableEq R] [Add R] (hzero : ∀ (c : R), 0 + c = c) (ts : Array (Nat × R)) (e : Nat) : (ofTerms ts).coeff e = Array.foldl (fun (a : R) (t : Nat × R) => a + t.snd) 0 (Array.filter (fun (t : Nat × R) => decide (t.fst = e)) ts)

The coefficient of ofTerms ts at e is the sum, in input order, of the coefficients of the terms of ts at e. The hzero hypothesis is what identifies a fresh insertion c with the fold's 0 + c; a coefficient type with Lean.Grind.Semiring discharges it from add_zero and add_comm.

def Hex.SparsePoly.combineRun {R : Type u} [Zero R] [DecidableEq R] [Add R] (e : Nat) (acc : R) : List (Nat × R) → List (Nat × R)

Combining worker for ofTermsImpl: walk a ≤-sorted term list with the run exponent e and its accumulated coefficient acc, replaying the addCoeff semantics of the addTerm fold within each equal-exponent block and emitting the nonzero results.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SparsePoly.combineRun e acc [] = if acc = 0 then [] else [(e, acc)]

def Hex.SparsePoly.combineSorted {R : Type u} [Zero R] [DecidableEq R] [Add R] : List (Nat × R) → List (Nat × R)

Combine the equal-exponent blocks of a ≤-sorted term list in one pass, dropping zero results.

Equations

• Hex.SparsePoly.combineSorted [] = []
• Hex.SparsePoly.combineSorted (t :: ts) = Hex.SparsePoly.combineRun t.fst (Hex.SparsePoly.addCoeff 0 t.snd) ts

theorem Hex.SparsePoly.combineRun_canonical {R : Type u} [Zero R] [DecidableEq R] [Add R] {l : List (Nat × R)} {e : Nat} {acc : R} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst ≤ b.fst) l) (hge : ∀ (t : Nat × R), t ∈ l → e ≤ t.fst) : List.Pairwise (fun (a b : Nat × R) => a.fst < b.fst) (combineRun e acc l) ∧ (∀ (t : Nat × R), t ∈ combineRun e acc l → t.snd ≠ 0) ∧ ∀ (t : Nat × R), t ∈ combineRun e acc l → e ≤ t.fst

The combining pass emits a canonical list whose exponents all lie at or above the run exponent.

theorem Hex.SparsePoly.coeffList_combineRun {R : Type u} [Zero R] [DecidableEq R] [Add R] {l : List (Nat × R)} {e : Nat} {acc : R} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst ≤ b.fst) l) (hge : ∀ (t : Nat × R), t ∈ l → e ≤ t.fst) (f : Nat) : coeffList (combineRun e acc l) f = if f = e then List.foldl (fun (a : R) (t : Nat × R) => addCoeff a t.snd) acc (List.filter (fun (t : Nat × R) => decide (t.fst = e)) l) else List.foldl (fun (a : R) (t : Nat × R) => addCoeff a t.snd) 0 (List.filter (fun (t : Nat × R) => decide (t.fst = f)) l)

Coefficient description of the combining pass: the run's own exponent reads its accumulator folded over the rest of its block, and every other exponent reads its whole block folded from 0.

theorem Hex.SparsePoly.coeffList_combineSorted {R : Type u} [Zero R] [DecidableEq R] [Add R] {l : List (Nat × R)} (hs : List.Pairwise (fun (a b : Nat × R) => a.fst ≤ b.fst) l) (f : Nat) : coeffList (combineSorted l) f = List.foldl (fun (a : R) (t : Nat × R) => addCoeff a t.snd) 0 (List.filter (fun (t : Nat × R) => decide (t.fst = f)) l)

Coefficient description of combineSorted on a ≤-sorted list: each exponent reads its block folded from 0.

theorem Hex.SparsePoly.filter_exp_mergeSort {R : Type u} {l : List (Nat × R)} (e : Nat) : List.filter (fun (t : Nat × R) => decide (t.fst = e)) (l.mergeSort fun (a b : Nat × R) => decide (a.fst ≤ b.fst)) = List.filter (fun (t : Nat × R) => decide (t.fst = e)) l

Stability of the exponent sort, in the form the combining pass needs: sorting by exponent does not reorder the terms within any one exponent's block.

def Hex.SparsePoly.ofTermsImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] (ts : Array (Nat × R)) : SparsePoly R

Runtime implementation of ofTerms: stable sort by exponent, then one combining pass, O(m log m) on m input terms against the specification's O(m²) worst case (value-equal to ofTerms by ofTerms_eq_impl, registered @[csimp]). Stability is load-bearing: it is what makes the per-block fold agree with the input-order fold of the specification with no algebra assumed.

Equations

• Hex.SparsePoly.ofTermsImpl ts = { terms := (Hex.SparsePoly.combineSorted (ts.toList.mergeSort fun (a b : Nat × R) => decide (a.fst ≤ b.fst))).toArray, canonical := ⋯ }

theorem Hex.SparsePoly.ofTerms_eq_ofTermsImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] (ts : Array (Nat × R)) : ofTerms ts = ofTermsImpl ts

The addTerm fold and the stable sort-and-combine pass build the same polynomial, with no algebra assumed.

@[csimp]

theorem Hex.SparsePoly.ofTerms_eq_impl : @ofTerms = @ofTermsImpl

Register the stable sort-and-combine pass as the compiled implementation of ofTerms.

def Hex.SparsePoly.monomial {R : Type u} [Zero R] [DecidableEq R] (e : Nat) (c : R) : SparsePoly R

The monomial c · x^e. The zero coefficient collapses to the zero polynomial.

Equations

• Hex.SparsePoly.monomial e c = if hc : c = 0 then 0 else { terms := #[(e, c)], canonical := ⋯ }

def Hex.SparsePoly.C {R : Type u} [Zero R] [DecidableEq R] (c : R) : SparsePoly R

The constant polynomial with value c. The zero constant collapses to the zero polynomial.

Equations

• Hex.SparsePoly.C c = Hex.SparsePoly.monomial 0 c

def Hex.SparsePoly.X {R : Type u} [Zero R] [DecidableEq R] [One R] : SparsePoly R

The variable x.

Equations

• Hex.SparsePoly.X = Hex.SparsePoly.monomial 1 1

@[instance_reducible]

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

Equations

• Hex.SparsePoly.instOne = { one := Hex.SparsePoly.C 1 }

@[simp]

theorem Hex.SparsePoly.coeff_monomial {R : Type u} [Zero R] [DecidableEq R] (e : Nat) (c : R) (f : Nat) : (monomial e c).coeff f = if f = e then c else 0

Characterising lemma for monomials: coefficient c at e, zero elsewhere, even when c = 0.

@[simp]

theorem Hex.SparsePoly.coeff_C {R : Type u} [Zero R] [DecidableEq R] (c : R) (f : Nat) : (C c).coeff f = if f = 0 then c else 0

A constant stores its value at exponent 0.

@[simp]

theorem Hex.SparsePoly.coeff_one {R : Type u} [Zero R] [DecidableEq R] [One R] (f : Nat) : coeff 1 f = if f = 0 then 1 else 0

The one polynomial is the constant 1.

@[simp]

theorem Hex.SparsePoly.coeff_X {R : Type u} [Zero R] [DecidableEq R] [One R] (f : Nat) : X.coeff f = if f = 1 then 1 else 0

The variable has coefficient 1 at exponent 1.

def Hex.sparsePolyLiteral : Lean.ParserDescr

#sp[(e₀, c₀), (e₁, c₁), …] constructs the canonical sparse polynomial with the given (exponent, coefficient) terms: any order, repeated exponents summed, zero coefficients dropped, mirroring #p[…] for DensePoly.

Equations

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