structure Hex.MvPoly (n : Nat) (R : Type u) [Zero R] (cmp : Mono n → Mono n → Ordering) [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : Type u

A canonical distributed multivariate polynomial. The backing tree map stores only nonzero coefficients and uses the explicit comparator cmp.

• termsInternal : Std.ExtTreeMap (Mono n) R cmp

  Internal backing map. Consumers should use termsList, foldTerms, monomials, and termCount so the representation can change.

• nonzeroInternal (m : Mono n) : self.termsInternal[m]? ≠ some 0

  Canonical-form invariant: zero coefficients are absent.

@[inline]

def Hex.MvPoly.coeff? {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (m : Mono n) (p : MvPoly n R cmp) : Option R

The absent coefficient of a monomial.

Equations

• Hex.MvPoly.coeff? m p = p.termsInternal[m]?

@[inline]

def Hex.MvPoly.coeff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (m : Mono n) (p : MvPoly n R cmp) : R

Coefficient of a monomial, returning zero outside the support.

Equations

• Hex.MvPoly.coeff m p = (Hex.MvPoly.coeff? m p).getD 0

def Hex.MvPoly.termsList {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : List (Mono n × R)

Ordered term list, in increasing cmp order.

Equations

• p.termsList = p.termsInternal.toList

def Hex.MvPoly.toList {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : List (Mono n × R)

Compatibility spelling for consumers that iterate over all terms.

Equations

• p.toList = p.termsList

@[inline]

def Hex.MvPoly.foldTerms {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] {α : Type u_1} (f : α → Mono n → R → α) (init : α) (p : MvPoly n R cmp) : α

Fold over terms in increasing cmp order.

Equations

• Hex.MvPoly.foldTerms f init p = Std.ExtTreeMap.foldl f init p.termsInternal

def Hex.MvPoly.monomials {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : List (Mono n)

Monomials in the support, in increasing cmp order.

Equations

• p.monomials = List.map Prod.fst p.termsList

def Hex.MvPoly.support {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : List (Mono n)

Monomials in the support, in increasing cmp order.

Equations

• p.support = p.monomials

theorem Hex.MvPoly.monomials_nodup {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : p.monomials.Nodup

The canonical support enumeration contains no duplicate monomials.

theorem Hex.MvPoly.mem_monomials_iff_isSome {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (m : Mono n) (p : MvPoly n R cmp) : m ∈ p.monomials ↔ (coeff? m p).isSome = true

A monomial occurs in the ordered monomial list exactly when coefficient lookup succeeds.

@[simp]

theorem Hex.MvPoly.mem_monomials_iff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (m : Mono n) (p : MvPoly n R cmp) : m ∈ p.monomials ↔ coeff m p ≠ 0

A monomial occurs in the ordered monomial list exactly when its coefficient is nonzero.

@[simp]

theorem Hex.MvPoly.mem_support_iff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (m : Mono n) (p : MvPoly n R cmp) : m ∈ p.support ↔ coeff m p ≠ 0

Membership in the support is equivalent to having a nonzero coefficient.

theorem Hex.MvPoly.coeff_eq_zero_of_not_mem {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (m : Mono n) (p : MvPoly n R cmp) (h : ¬m ∈ p.monomials) : coeff m p = 0

A monomial outside the canonical support has coefficient zero.

theorem Hex.MvPoly.coeff_eq_of_mem_terms {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) {m : Mono n} {c : R} (h : (m, c) ∈ p.termsList) : coeff m p = c

A stored term carries exactly the coefficient returned by lookup.

@[inline]

def Hex.MvPoly.termCount {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : Nat

Number of nonzero terms.

Equations

• p.termCount = p.termsInternal.size

@[inline]

def Hex.MvPoly.maxTerm? {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) : Option (Mono n × R)

Greatest term in cmp order.

This uses the tree's logarithmic maximum-key query followed by one logarithmic lookup. Keeping the definition in terms of the public key and lookup API gives downstream proofs access to the complete maximum-entry specification even though Std.ExtTreeMap.maxEntry? currently lacks corresponding lemmas.

Equations

• p.maxTerm? = p.termsInternal.maxKey?.bind fun (m : Hex.Mono n) => Option.map (fun (c : R) => (m, c)) p.termsInternal[m]?

theorem Hex.MvPoly.maxTerm?_eq_some_iff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) (m : Mono n) (c : R) : p.maxTerm? = some (m, c) ↔ coeff? m p = some c ∧ ∀ (k : Mono n), k ∈ p.monomials → (cmp k m).isLE = true

A maximum term is exactly a stored coefficient whose monomial bounds every supported monomial in cmp order.

def Hex.MvPoly.zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] : MvPoly n R cmp

The zero polynomial.

Equations

• Hex.MvPoly.zero = { termsInternal := ∅, nonzeroInternal := ⋯ }

@[instance_reducible]

instance Hex.MvPoly.instZero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] : Zero (MvPoly n R cmp)

Equations

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

@[instance_reducible]

instance Hex.MvPoly.instInhabited {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] : Inhabited (MvPoly n R cmp)

Equations

• Hex.MvPoly.instInhabited = { default := 0 }

theorem Hex.MvPoly.coeff?_ne_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (p : MvPoly n R cmp) (m : Mono n) : coeff? m p ≠ some 0

The stored representation contains no explicit zero coefficient.

theorem Hex.MvPoly.ext {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] {p q : MvPoly n R cmp} (h : ∀ (m : Mono n), coeff m p = coeff m q) : p = q

Coefficients determine a canonical multivariate polynomial.

theorem Hex.MvPoly.ext_iff {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] {p q : MvPoly n R cmp} : p = q ↔ ∀ (m : Mono n), coeff m p = coeff m q

@[instance_reducible]

instance Hex.MvPoly.instBEqOfDecidableEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [DecidableEq R] : BEq (MvPoly n R cmp)

Boolean equality compares ordered term lists, avoiding the tree map's derived equality implementation in the kernel replay path.

Equations

• Hex.MvPoly.instBEqOfDecidableEq = { beq := fun (p q : Hex.MvPoly n R cmp) => decide (p.termsList = q.termsList) }

instance Hex.MvPoly.instLawfulBEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [DecidableEq R] : LawfulBEq (MvPoly n R cmp)

@[instance_reducible]

instance Hex.MvPoly.instDecidableEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [DecidableEq R] : DecidableEq (MvPoly n R cmp)

Equations

• p.instDecidableEq q = match decEq p.termsList q.termsList with | isTrue hl => isTrue ⋯ | isFalse hl => isFalse ⋯

def Hex.MvPoly.monomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [BEq R] [LawfulBEq R] (m : Mono n) (c : R) : MvPoly n R cmp

A single term, dropping it when its coefficient is zero.

Equations

• Hex.MvPoly.monomial m c = if hc : c = 0 then 0 else { termsInternal := ∅.insert m c, nonzeroInternal := ⋯ }

def Hex.MvPoly.C {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [BEq R] [LawfulBEq R] (c : R) : MvPoly n R cmp

A constant polynomial.

Equations

• Hex.MvPoly.C c = Hex.MvPoly.monomial Hex.Mono.zero c

def Hex.MvPoly.X {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [One R] [BEq R] [LawfulBEq R] (i : Fin n) : MvPoly n R cmp

The variable xᵢ.

Equations

• Hex.MvPoly.X i = Hex.MvPoly.monomial (Hex.Mono.unit i) 1

def Hex.MvPoly.addMonomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Add R] [BEq R] [LawfulBEq R] (p : MvPoly n R cmp) (m : Mono n) (c : R) : MvPoly n R cmp

Add c to the coefficient at m, deleting the term if the new coefficient is zero.

Equations

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

def Hex.MvPoly.ofTerms {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Add R] [BEq R] [LawfulBEq R] (ts : List (Mono n × R)) : MvPoly n R cmp

Build a polynomial by summing duplicate monomials and dropping all zero coefficients. Only additive structure is needed by the constructor.

Equations

• Hex.MvPoly.ofTerms ts = List.foldl (fun (p : Hex.MvPoly n R cmp) (t : Hex.Mono n × R) => p.addMonomial t.fst t.snd) 0 ts

@[simp]

theorem Hex.MvPoly.coeff_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] (m : Mono n) : coeff m 0 = 0

Every coefficient of the zero polynomial is zero.

theorem Hex.MvPoly.coeff_monomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [BEq R] [LawfulBEq R] [DecidableEq R] (m m' : Mono n) (c : R) : coeff m (monomial m' c) = if m = m' then c else 0

A monomial polynomial has its supplied coefficient at the selected monomial and zero elsewhere.

theorem Hex.MvPoly.coeff_C {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [BEq R] [LawfulBEq R] [DecidableEq R] (m : Mono n) (c : R) : coeff m (C c) = if m = Mono.zero then c else 0

A constant polynomial is supported at the zero monomial.

theorem Hex.MvPoly.coeff_X {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [One R] [BEq R] [LawfulBEq R] [DecidableEq R] (m : Mono n) (i : Fin n) : coeff m (X i) = if m = Mono.unit i then 1 else 0

A variable polynomial is supported at its unit monomial.

theorem Hex.MvPoly.coeff_addMonomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [Add R] [BEq R] [LawfulBEq R] [DecidableEq R] (p : MvPoly n R cmp) (m k : Mono n) (c : R) : coeff k (p.addMonomial m c) = if k = m then coeff k p + c else coeff k p

Adding a monomial changes only the selected coefficient.

theorem Hex.MvPoly.coeff_ofTerms {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (m : Mono n) (ts : List (Mono n × R)) : coeff m (ofTerms ts) = List.foldl (fun (acc : R) (t : Mono n × R) => acc + t.snd) 0 (List.filter (fun (t : Mono n × R) => decide (t.fst = m)) ts)

ofTerms sums the coefficients of duplicate monomials.

theorem Hex.MvPoly.coeff_terms {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (m : Mono n) (p : MvPoly n R cmp) : List.foldl (fun (acc : R) (t : Mono n × R) => acc + t.snd) 0 (List.filter (fun (t : Mono n × R) => decide (t.fst = m)) p.termsList) = coeff m p

Filtering the canonical term list at one monomial recovers its coefficient.