hex

5.3.ย The polynomial type๐Ÿ”—

Hex.MvPoly bundles an ordered tree map with the invariant that no stored coefficient is zero. Duplicate terms are combined and cancellations are deleted, leaving one representation for each polynomial.

๐Ÿ”—structure
Hex.MvPoly.{u} (n : โ„•) (R : Type u) [Zero R]
  (cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering) [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type u
Hex.MvPoly.{u} (n : โ„•) (R : Type u)
  [Zero R]
  (cmp :
    Hex.Mono n โ†’ Hex.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.

Constructor

Hex.MvPoly.mk.{u}

Fields

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

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

nonzeroInternal : โˆ€ (m : Hex.Mono n), self.termsInternal[m]? โ‰  some 0

Canonical-form invariant: zero coefficients are absent.

The tree is an implementation detail. Construction and inspection go through the following API:

๐Ÿ”—def
Hex.MvPoly.monomial.{u} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] [BEq R] [LawfulBEq R] (m : Hex.Mono n)
  (c : R) : Hex.MvPoly n R cmp
Hex.MvPoly.monomial.{u} {n : โ„•}
  {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] [BEq R] [LawfulBEq R]
  (m : Hex.Mono n) (c : R) :
  Hex.MvPoly n R cmp

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

๐Ÿ”—def
Hex.MvPoly.C.{u} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] [BEq R] [LawfulBEq R] (c : R) :
  Hex.MvPoly n R cmp
Hex.MvPoly.C.{u} {n : โ„•} {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] [BEq R] [LawfulBEq R] (c : R) :
  Hex.MvPoly n R cmp

A constant polynomial.

๐Ÿ”—def
Hex.MvPoly.X.{u} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] [One R] [BEq R] [LawfulBEq R]
  (i : Fin n) : Hex.MvPoly n R cmp
Hex.MvPoly.X.{u} {n : โ„•} {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] [One R] [BEq R] [LawfulBEq R]
  (i : Fin n) : Hex.MvPoly n R cmp

The variable xแตข.

๐Ÿ”—def
Hex.MvPoly.ofTerms.{u} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] [Add R] [BEq R] [LawfulBEq R]
  (ts : List (Hex.Mono n ร— R)) : Hex.MvPoly n R cmp
Hex.MvPoly.ofTerms.{u} {n : โ„•}
  {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] [Add R] [BEq R] [LawfulBEq R]
  (ts : List (Hex.Mono n ร— R)) :
  Hex.MvPoly n R cmp

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

๐Ÿ”—def
Hex.MvPoly.coeff.{u} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] (m : Hex.Mono n)
  (p : Hex.MvPoly n R cmp) : R
Hex.MvPoly.coeff.{u} {n : โ„•} {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] (m : Hex.Mono n)
  (p : Hex.MvPoly n R cmp) : R

Coefficient of a monomial, returning zero outside the support.

๐Ÿ”—def
Hex.MvPoly.termsList.{u} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] (p : Hex.MvPoly n R cmp) :
  List (Hex.Mono n ร— R)
Hex.MvPoly.termsList.{u} {n : โ„•}
  {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] (p : Hex.MvPoly n R cmp) :
  List (Hex.Mono n ร— R)

Ordered term list, in increasing cmp order.

๐Ÿ”—def
Hex.MvPoly.foldTerms.{u, u_1} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] {ฮฑ : Type u_1}
  (f : ฮฑ โ†’ Hex.Mono n โ†’ R โ†’ ฮฑ) (init : ฮฑ) (p : Hex.MvPoly n R cmp) : ฮฑ
Hex.MvPoly.foldTerms.{u, u_1} {n : โ„•}
  {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] {ฮฑ : Type u_1}
  (f : ฮฑ โ†’ Hex.Mono n โ†’ R โ†’ ฮฑ) (init : ฮฑ)
  (p : Hex.MvPoly n R cmp) : ฮฑ

Fold over terms in increasing cmp order.

๐Ÿ”—def
Hex.MvPoly.termCount.{u} {n : โ„•} {R : Type u}
  {cmp : Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Zero R] (p : Hex.MvPoly n R cmp) : โ„•
Hex.MvPoly.termCount.{u} {n : โ„•}
  {R : Type u}
  {cmp :
    Hex.Mono n โ†’ Hex.Mono n โ†’ Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Zero R] (p : Hex.MvPoly n R cmp) : โ„•

Number of nonzero terms.

The reusable map machinery is kept below the polynomial layer in HexBasic/ExtTreeMap.lean. Its deletion-capable merge API is independent of coefficient types and polynomial policy, making that file a candidate for later upstreaming. HexMvPoly supplies only the coefficient combination and zero-elision rules.